Re: [isabelle] unicode tokens in isabelle2011+pg4.0

Hi John,

I don't think this will work with PG 4.0. I use ProofGeneral-4.1pre110131. In order to get rid of boxes displayed instead of symbols, set the buffer's font to "Apple Symbols". Also set the symbol font in "Tokens > Set Font > symbol" to this font.

You may choose a different font for the buffer, but then symbols in antiquotations won't work.


Quoting John Wickerson <jpw48 at>:


I've just upgraded from Isabelle2009-2 to Isabelle2011, and from pg3.7 to pg4.0. (I'm running Aquamacs 2.1.)

The upgrade was fine, except I'm now having a problem with unicode tokens.

I have my keyboard layout set up so that, for instance, OPTION-SHIFT-A produces the unicode forall (?) symbol. Previously I could use this freely in Isabelle proof scripts, but now I get an "inner lexical error" message when Isabelle is parsing statements involving these symbols.

When I turn on "highlight real unicode chars" in the Tokens menu, this forall symbol is highlighted, but when I type "\<forall>" in my proof script, it produces a symbol that *looks* the same as the unicode character, but isn't highlighted.

How can I get back my ability to write my isabelle scripts in unicode?

Thanks very much for your help.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.