mailing-list for TeXmacs Users

[Jeroen Wouters <address@hidden>]

Dear Max,

It looks like this is the actual display size. There is a clear visual
difference between the output size of text in Liberation Sans 11pt font
between TeXmacs, LaTeX and LibreOffice Writer.

The Liberation Sans font was installed with the package manager of my
Linux distribution. It can also be downloaded here:
https://github.com/liberationfonts/liberation-fonts/releases

Most fonts give an exact 11pt output in TeXmacs, but I have found a few
fonts for which the PDF font size differs from the selected 11pt
(Liberation Sans 9.42pt, PT Sans 11.48pt, DejaVu Sans 10.35).

Best wishes,
Jeroen

On Sat, 2022-01-15 at 19:40 +0100, Massimiliano Gubinelli wrote:
> Dear Jeroen,
>  are you sure the size mentioned by Acrobat is not the design size of
> the font? Where do TeXmacs take the font? Have you installed it
> yourself? (I do not have it on my Mac)
> 
> Max
> 
> 
> > On 15. Jan 2022, at 09:03, Jeroen Wouters <address@hidden>
> > wrote:
> > 
> > Hello fellow TeXmacs users,
> > 
> > I recently decided to use TeXmacs to compose a document for
> > submission
> > to a UK funding agency. They can be notoriously strict about the
> > font
> > size used in submitted documents, so I double checked the font size
> > of
> > the PDF before submission.
> > 
> > I was surprised to find that the font size was quite a bit off from
> > what was selected in TeXmacs. A 11pt Liberation Sans font comes out
> > as
> > 9.42pt in the PDF (checked in both Inkscape and Adobe Reader).
> > 
> > Different fonts result in different sizes, some larger and some
> > smaller
> > than what was selected. Liberation Sans was the most extreme case,
> > but
> > it is the font I need to use for this document.
> > 
> > I realize that LaTeX does something similar, but there the results
> > are
> > less extreme (Liberation Sans 11pt resulting in a 10.91pt output
> > font).
> > LibreOffice Writer outputs at exactly 11pt.
> > 
> > Does anyone know how the font size of the PDF is calculated? Is
> > there
> > any way to set an exact PDF font size?
> > 
> > Best wishes,
> > Jeroen
>