Re: [isabelle] unicode tokens in isabelle2011+pg4.0
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 cam.ac.uk>:
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