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 which happens to be 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 MHonArc.