[isabelle-dev] misc problems

[Andrew Boyton]

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