Email Gateway (Aug 19 2022 at 08:39): Email Gateway (Aug 19 2022 at 08:39):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I've been having a strange problem with Proof General lately: whenever I
start Proof General, "Display Unicode Tokens" is disabled. I can enable
it and it will work, but even when I save the settings, it will be
disabled again upon the next start of Proof General. In fact, merely
opening another file switches it off - but only for the buffer
containing that file, if I switch back to the other buffer, it's
switched on again.
This problem occurs only on my laptop, which runs a 32 bit Ubuntu 12.04
with emacs version 24.1.50.1 and the latest Isabelle 2012 from the
website. I have tried deleting all emacs configuration files I could
find and completely reinstalling Isabelle but the problem remained.
Another, possibly related, problem is that proof hiding does not work.
Whenever a proof is processed completely, all the Unicode tokens
disappear in the processed portion of the input, i.e. I see
\<Longrightarrow> instead of ⟹.
I realise that this is a minor issue and the development of Proof
General is in a bit of a limbo at the moment, but this is starting to
rather annoy me and I thought it might be a good idea to ask on the
mailing list in order to find out of somebody else is experiencing the
same problems and knows a fix.
Cheers,
Manuel
Last updated: Nov 21 2024 at 12:39 UTC