Re: [isabelle] ProofGeneral font-lock-mode and antiquoatations
On Fri, 24 Jul 2009, Christian Doczkal wrote:
If I open Emacs/ProofGeneral and load todays version of "FirstSteps.thy"
and scroll down emacs just hangs (100% CPU, no reaction for minutes,
sometimes it comes back). If I disable font-lock mode this problem
disappears. No Isabelle process running at this time
I suspect this has something to do with the antiquotations in the text
blocks. I had similar problems before but only with antiquotations whose
parenthesis do not match.
Loosely related: There seems to be an error in the text block beginning
at in lines 978-1009. Isabelle (yesterdays development snapshot) refused
to check this block with error message:
I use Emacs (22.2.1) and ProofGeneral (3.7.1) on Ubuntu 9.04 AMD64. Can
someone reproduce this error? Is there a workaround except disabling
This is a known problem of Proof General 3.7.1 running on GNU Emacs.
Maybe this helps:
Anyway, what is "todays version of FirstSteps.thy"? I have never heard of
such a file in the Isabelle repository. "Yesterdays development snapshot"
is also hard to pin down.
With distributed version control (Mercurial), one needs to refer to
versions via the official id -- commit dates don't count. In Isabelle
development snapshots this is printed as "welcome" message of
isabelle-process or by "isabelle version".
Or you can just refer to the full URL, e.g. via the link on
http://isabelle.in.tum.de/devel which happens to be
http://isabelle.in.tum.de/repos/isabelle/changelog/f01207d56583 right now.
As usual, one needs to have very strong reasons to "use" a development
snapshot instead of a proper release. In particularly, one needs to keep
an eye on the Mercurial history all the time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and