Re: [isabelle] Secondary Fonts in symbols file Re: Announcing Isabelle2019

On 19/06/2019 04:29, Dr. Brendan Patrick Mahony wrote:
>> On 11 Jun 2019, at 7:10 am, Makarius <makarius at> wrote:
>> * Improved "Isabelle DejaVu" font collection, suitable for text and GUI.
> Sorry to be late to this party. The new fonts look great on my 15” MacBook Pro.

(This merely means that I am now extra-late to answer this, after the
Isabelle2019 release and the travels after are finished.)

> My query is about the use of secondary fonts. 
> For example: 
> \<xexprel>              code: 0x00e18D  group: 3xMath font: IsabelleTextStix
> In Isabelle 2019 this font now renders at about 2/3 size.
> Is this a known thing? Is there some Jedit setting I can adjust?

I don't know if it should be known. Java font management has always been
a bit strange, and Java 11 (Isabelle2019) changes many things over Java
8 (Isabelle2018).

The relevant operation in Isabelle/Scala is GUI.imitate font. You can
try it in the Console/Scala window of Isabelle/jEdit like this:

scala> val font1 = view.getTextArea.getPainter.getFont
font1: java.awt.Font = java.awt.Font[family=Isabelle DejaVu Sans
Mono,name=Isabelle DejaVu Sans Mono,style=plain,size=36]
scala> val font2 = GUI.imitate_font(font1, "STIXGeneral")
font2: java.awt.Font =

> Can I “scale” the IsabelleTextStix font in the symbols file?

Is this a home-made font? You could use fontforge to change its relative
size, but I don't understand all fine points of this sophisticated tool.

Isabelle/Scala now provides the administrative tool "build_fonts" to run
fontforge in batch-mode to assemble glyphs from various fonts, using
DejaVu as the basis, which also defines the overall metrics. This is
also the reason for the change (improvement) of Isabelle font sizes in
Isabelle2019. See
for details.

That follows the general principle of current Isabelle font handling:
all special glyphs are internalized into the main font, extra font
substitutions are avoided.


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