Re: [isabelle] Fwd: Re: Unicode tokens

Tim's investigation of behaviour is useful (thanks). At a risk of repeating myself, the summary from my point of view is:

- XSymbol is not compatible with Emacs 23,.

- Unicode Tokens is experimental in PG 3.7.1.(1) I do not recommend using it with sub/superscripts. Please read the CHANGES file in the PG distribution. PG 4.0 has a better implementation.

- Mixing Unicode Tokens and X-Symbol in the same session is a recipe for disaster!

I don't understand the comment about the Format menu. There are two sub-menus, "Format Char" and "Format Region". Items in Format Region are greyed out unless there is an active (selected) region.

 - David

Tim McKenzie wrote:
On Tue, 08 Dec 2009 21:39:48 you wrote:
msg deleted, sorry, pls resend!
Larry Paulson

Sorry; I intended to send this message to the list the first time around; I replied to all on a previous message, and didn't notice that the list wasn't included.

Thanks for your advice, everyone. I've done a bit more testing with Proof General 3.7.1 and and Emacs 22 and 23. Although my testing hasn't been exhaustive, here are my conclusions:

If X-Symbol has been active, but is then turned off, then when Unicode tokens are turned on, any instances of \<^sub> will disappear (causing Isabelle to refuse to process the buffer), but only when you scroll up or down to where they are in the buffer --- if none are visible when you turn Unicode tokens on, then you can still successfully process the whole buffer. As long as X-
Symbol is never turned on this problem doesn't occur.

With Unicode tokens turned on, I can enter and process \<^sub> correctly, but the next character doesn't actually appear as a subscript. To get, for example, a * with a subscript R, I can copy and paste it from the output buffer, or I can type *\<^sub>R and then turn Unicode tokens off and back on again. This is annoying, but I can live with it for now.

When Unicode tokens are turned on, everything in the Format menu is greyed out.


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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