> 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev