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

Hi John,

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.

The handling of symbols changed drastically from pg 3.7 to 4.

I am not sure if I know a solution, but the problem seems to be that you are creating a unicode symbol in the buffer, but Isabelle expects the ascii-encoded symbol \<forall> (which pg displays using the same glyph, but it's represented differently). I can reproduce this without special keyboard mapping by copy and pasting the character from elsewhere.

I haven't seen an option in pg that rebinds unicode keysyms to these special tokens. However, in the worst case you should be able to rebind the keys yourself. Here is what works in my Emacs:

(global-set-key (kbd "C-A") (lambda () (interactive)
  (unicode-tokens-insert-token "forall")))

(possibly replacing the unicode keysym for C-A)
Unfortunately, you have to do this for each symbol then... but it's better than nothing.

Hope this helps...

Clemens Ballarin wrote:
In order to get rid of boxes displayed instead of symbols...

Do I understand correctly that you do see the symbols correctly...?


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