[isabelle-dev] misc problems

[Andrew Boyton]

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