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
font-lock-mode?

This is a known problem of Proof General 3.7.1 running on GNU Emacs. Maybe this helps:

http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/rev/36eccb23fddf


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.


	Makarius





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