Re: [isabelle] ProofGeneral 3.7pre071112 gets out of sync with Isabelle process



On Wed, 28 Nov 2007, Peter Lammich wrote:

> Here is a reproducible way to get ProofGeneral  3.7pre071112 out of sync
> with the isabelle2007 process, simply process this theory:
> 
> theory Scratch
> imports Main
> begin
> 
>   lemma X: "a=b ==> b=a" by simp
>   -- "Text with \illegal escape sequence"
> 
> end

The very same happens with Isabelle2005 and Proof General 3.6pre050930 -- 
the combination we've shipped more than two years ago.  I'd guess this 
issue dates back a few more years in the past, when the "--" annotation 
was introduced.  (The loss of sync is caused by a token-level error in 
Isabelle, such that Proof General gets the wrong idea about which part of 
the text belongs to the ``command span''.  The use of "--" is critical 
here, other situations should be OK.)

There is no easy fix for the moment, but it should not take another 5 
years to make it work properly ...


	Makarius





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