On Tue, 20 Sep 2011, René Thiemann wrote:

when using the September 2011 version, I spotted the following font problem under Mac OS Lion:

record braces \<lparr> and \<rparr> are displayed as blanks (although the width is roughly half of a normal blank)

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 -- this font includes a massive amount of mathematical symbols.

For the Isabelle.app script (see Isabelle.app/Contents/Resources/script), I am forcing that font onto the user as follows:


# enforce fonts

if [ ! -f "$HOME/Library/Fonts/STIXGeneral.ttf" -a ! -f 
"$HOME/Library/Fonts/STIXGeneral.otf" ]
then
  cp -f "$THIS/STIXv1.0.0/Fonts"/STIXGeneral* "$HOME/Library/Fonts/"
  sleep 3
fi


This used to satisfy Emacs in finding the required glyphs.

Since Mac OS X Lion seems to provide its own copy of STIX fonts -- according to the advertisement -- there is some potential for confusion. (I do not have Lion available right now on my desktop.)


In the end either Apple, Emacs or Proof General are to blame. If you can give some hints how to improve the workarounds in the the above script, I will amend this.

Moreover, for Isabelle_11-Sep-2011 I am still using the Emacs-23.2.1.app from Isabelle2011, but this is going to be the current Emacs-23.3.app in the coming release. There is a tiny chance that updating Emacs also solves the problem -- see the symlink Contents/Resources/Emacs.app


        Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to