Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts

2018-11-30 Thread Makarius
On 24/11/2018 19:51, Makarius wrote:
> 
> *** Isabelle/jEdit Prover IDE ***
> 
> * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
> DejaVu" collection by default, which provides uniform rendering quality
> with the usual Isabelle symbols. For Java/Swing GUI elements this
> requires the Metal look-and-feel: it is the default on Linux, but not
> macOS nor Windows. Line spacing no longer needs to be adjusted:
> properties for the old IsabelleText font had "Global Options / Text Area
> / Extra vertical line spacing (in pixels): -2", now it defaults to 0.

I have reworked this further in various changesets leading up to
Isabelle/429426640596. In particular, the Isabelle fonts are now forced
on all Java/Swing look-and-feels, by modifying some UIManager font
properties.

This appears to work reasonably well on Linux GTK+, Windows, Mac OS X,
but we need to keep an eye on it for fine points and drop-outs. (For
Metal look-and-feel and already worked uniformly before.)

The idea is that GUI elements use "Isabelle DejaVu Sans" (not "Mono")
wherever feasible. Thus all mathematical symbols and special  icons
should be always correctly displayed (e.g. in Hypersearch tree view).
The regular search dialog now also uses this font: before it was the
main text area font (usually the "Mono" version).


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts

2018-11-24 Thread Makarius
On 24/11/2018 19:51, Makarius wrote:
> *** General ***
> 
> * The font family "Isabelle DejaVu" is systematically derived from the
> existing "DejaVu" collection, 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).

Side-remark: this works via "isabelle build_fonts -d
dejavu-fonts-ttf-2.37/ttf"

The Isabelle/Scala sources of this tool should be obvious, see
http://isabelle.in.tum.de/repos/isabelle/file/395c4fb15ea2/src/Pure/Admin/build_fonts.scala


In the past, people have occasionally pointed out that the standard
Isabelle font is a bit boring. If there are other high-quality fonts to
be considered for the Isabelle font portfolio, I am interested to hear
about them.

Of course, it is also possible to use private Isabelle-derivatives of
existing fonts, such as some Apple fonts that are provided with macOS.
(These are usually non-free and we cannot ship them by default.)

It is generally better to have all special glyphs in a single font where
all sizes are carefully fit together, instead of implicit or explicit
multi-font assembly in GUI frameworks.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


[isabelle-dev] NEWS: Isabelle DejaVu fonts

2018-11-24 Thread Makarius
*** General ***

* The font family "Isabelle DejaVu" is systematically derived from the
existing "DejaVu" collection, 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.


* The Isabelle fonts render "¯" properly as superscript "-1".

*** Isabelle/jEdit Prover IDE ***

* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
DejaVu" collection by default, which provides uniform rendering quality
with the usual Isabelle symbols. For Java/Swing GUI elements this
requires the Metal look-and-feel: it is the default on Linux, but not
macOS nor Windows. Line spacing no longer needs to be adjusted:
properties for the old IsabelleText font had "Global Options / Text Area
/ Extra vertical line spacing (in pixels): -2", now it defaults to 0.

* Improved sub-pixel font rendering (especially on Linux), thanks to
OpenJDK 11.


This refers to Isabelle/395c4fb15ea2 and Isabelle/6aa24ccd8049.

The idea to construct Isabelle fonts systematically with the fontforge
scripting language has been in the pipeline for a long time. It has now
been flushed due to the change of font-rendering in the OpenJDK 11
version that we are using: now we have proper bold-italic fonts as well,
which is relevant to render control symbols like \<^term>.

I have taken the opportunity to brush-up the whole font setup, such that
we are again a little better of than before, according to the strict
monotonicity principle of Isabelle development.


Users hooked on isabelle-dev versions might have to revisit their
Isabelle/jEdit properties, to ensure that no "IsabelleText" font
specifications are left. Already existing user properties take
precedence over defaults provided by Isabelle/jEdit: see
$ISABELLE_HOME_USER/jedit/properties vs.
$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props and recall that the
"properties" file cannot be changed while Isabelle/jEdit is running (it
will be overwritten on application shutdown).


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev