[isabelle-dev] Unicode tokens and Isabelle fonts

Makarius makarius at sketis.net
Wed Jul 29 14:50:54 CEST 2009

On Wed, 29 Jul 2009, Lucas Dixon wrote:

> I've been using the Unicode tokens with Proof General (PG 3.7.1, Emacs
>, Using the IsabelleMono font), and thought I should give a
> little feedback (in order of importance, I think):
> Is there plans to develop the Isabelle font further?

Font design is a very delicate thing, and it is almost impossible to 
produce a homegrown font that actually works in practice.  IsabelleMono 
also has a number of internal technical problems with the curves that can 
make some ttf libraries on Windows crash, for example.

After declaring that I would never produce a font again (2 years ago), I 
ended up publishing IsabelleMono as an intermediate workaround in order to 
be able to see something on unicode-only editor views.  I am still hoping 
that the STIX project will deliver something after all these years, see 

Their struggle probably shows how difficult mathematical font design 
actually is.  Or maybe these guys are just clueless?


More information about the isabelle-dev mailing list