If this is indeed cause of the symbols problem, then in Font Book, I disabled 
all but the "Regular" version STIXGeneral font (there is Italics, Bold and Bold 
Italics). I left all of the other versions of  STIX fonts.

Andrew


On 19/03/2012, at 7:14 PM, Lawrence Paulson wrote:

> I am using OS X Lion. But the system software is the same on machines where 
> it works and those where it doesn't.
> 
> There are 29 of these fonts. Which ones are specifically needed for Isabelle? 
> Did you delete a specific file from Library/Fonts?
> 
> Larry
> 
> On 19 Mar 2012, at 04:44, Andrew Boyton wrote:
> 
>> I found on OS X Lion that it was best to disable the italics STIX fonts 
>> system wide, as Isabelle tried to use the italics version (which didn't have 
>> glyphs for all of the symbols).
>> 
>> Disabling the italics version of STIX systemwide was overkill, but easy to 
>> do in Font Book. STIX is now included in OS X by default, so maybe the 
>> problem was conflict between the default version and Isabelle's own STIX 
>> font that is included, I'm not sure. This could also be fixed by making 
>> Emacs not use the italics version, but I was unable to manage that.
>> 
>> I am unsure why Emacs needs symbol fonts anyway, as OS X has fallback 
>> mechanisms in every other text editor to use a custom symbol font whenever 
>> the font in question doesn't have the required symbol.
>> 
>> Out of curiosity/help with diagnosis, what operating system are you running?
>> 
>> Hope this helps.
>> Andrew
>> 
>> On 18/03/2012, at 9:34 PM, Lawrence Paulson wrote:
>> 
>>> I'm doing a demo this week, and find that some symbols don't display 
>>> properly on my laptop. I've installed the STIX fonts and tried to make 
>>> everything the same as my desktop. Most symbols work, but not \<lesssim> or 
>>> even \<times>. Any ideas?
>>> 
>>> Another thing: what's this?
>>> 
>>> ### load_lib </Users/lp15/isabelle/polyml/x86-darwin/libsha1.so> : 
>>> dlopen(/Users/lp15/isabelle/polyml/x86-darwin/libsha1.so, 1): image not 
>>> found
>>> ### Using slow ML implementation of SHA1.digest
>>> 
>>> Larry
>>> 
>>> <Screen Shot 2012-03-18 at 10.03.39.jpg>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> [email protected]
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 

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

Reply via email to