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 22.214.171.124 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 <><
Description: This is a digitally signed message part.