[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
> 23.0.93.1, 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 
http://www.aip.org/stixfonts/

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


 	Makarius



More information about the isabelle-dev mailing list