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
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.
Tim McKenzie wrote:
On Tue, 08 Dec 2009 21:39:48 you wrote:
msg deleted, sorry, pls resend!
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 188.8.131.52 and Emacs 22 and 23.
Although my testing hasn't been exhaustive, here are my
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