[isabelle] ProofGeneral font-lock-mode and antiquoatations



Hello

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:

*** Outer lexical error: missing end of verbatim text at     Unfort ...
*** Outer syntax error: document source expected,
*** but bad input {* was found
*** Outer lexical error: missing end of verbatim text at     Unfort ...
*** Outer lexical error: bad input at \emph{not} ...
*** Outer lexical error: bad input at \mbox{ at {te ...
*** missing quote at end of string at (@; \<^sync>;

If I remove this text block isabelle checks the document without errors,
but the ProofGerenal/font-lock-mode problem persists.

----------------------------------------------------------------------

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?


-- 
Christian Doczkal <doczkal at ps.uni-sb.de>






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