[isabelle-dev] Towards release

[David Aspinall]

> We have had this problem before with Isabelle2011.  PG 4.x has a certain 
> idea about using glyphs from existing Unicode fonts, with a preference for 
> STIXGeneral as fall-back option 

As you'd expect, this is all highly configurable at PG level (see
lib/unicode-tokens.el and isar/isar-unicode-tokens.el), I just set
picked some reasonable default fonts and Unicode points which worked
well when I wrote the code 3 years ago.  I welcome improvements from
anyone.

By default all symbols are taken from a single Unicode font, which seems
simplest and most sensible with the advent of STIX.  There are
mechanisms to try to choose fallback symbol renderings automatically,
which can be taken glyphs or sequences of glyphs from other fonts (see
isar-symbols-tokens-fallbacks).  But the automation is tricky because
the functions to determine whether a glyph is blank or not are not
reliable.

Mac users should be aware that there are issues with the underlying font
support on the native Mac port of Emacs, although a couple of these have
been fixed recently they haven't made it into a released version yet.  

http://proofgeneral.inf.ed.ac.uk/trac/ticket/338
http://proofgeneral.inf.ed.ac.uk/trac/ticket/409

I think the worst problem is broken super/sub scripts.  I've checked
that this *is* fixed now in the current nightly builds at
http://emacsformacosx.com/builds, but it's probably not a good idea to
bundle one of those with the release, 8-(.

 - David



-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.