Re: [isabelle] Fwd: Re: Unicode tokens



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

Tim
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



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