[isabelle-dev] Towards release

Makarius makarius at sketis.net
Tue Sep 20 14:49:12 CEST 2011

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" ]
   cp -f "$THIS/STIXv1.0.0/Fonts"/STIXGeneral* "$HOME/Library/Fonts/"
   sleep 3

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


More information about the isabelle-dev mailing list