Re: [isabelle] Isabelle2019-RC0: Improved "Isabelle DejaVu" font collection, suitable for text and GUI



On 05/04/2019 22:54, Makarius wrote:
> 
> *** General ***
> 
> * The font collection "Isabelle DejaVu" is systematically derived from
> the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
> and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
> The DejaVu base fonts are retricted to well-defined Unicode ranges and
> augmented by special Isabelle symbols, taken from the former
> "IsabelleText" font (which is no longer provided separately). The line
> metrics and overall rendering quality is closer to original DejaVu.
> INCOMPATIBILITY with display configuration expecting the old
> "IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.

One more hint: "Isabelle DejaVu Sans Mono" is still the default for the
main text area, but it is also possible to use the proportional font
"Isabelle DejaVu Sans" instead (or even "Isabelle DejaVu Serif", but
that looks odd to me).

I am not using propertional fonts regularly yet, but have started to
give occasional Isabelle demos with that configuration. After all, the
formal theory text is meant to be a true document, as in LibreOffice or
MS Word (with formal "spell-checking").

The proportional font helps to emphasize this idea, especially to people
who think about proofs as "program code", but also to others who are not
familiar with programming (or "coding").


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.