[isabelle] unicode tokens in isabelle2011+pg4.0



Hello,

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.
John




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