[isabelle] unicode tokens in isabelle2011+pg4.0
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