Out of sync on illegal escape character

[Peter Lammich]

PG-Emacs: 3.7pre071112 Isabelle: 2007

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

This happens quite often if you insert latex in your formal comment and forget to convert "..." to {*...*} syntax. Having to restart Isabelle each time is annoying for large theories.

[David Aspinall]

Thanks for reporting here. Reply on Isabelle mailing list from Makarius:

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 essentially needs to be fixed on the Isabelle side, even though Proof General is the one to get confused here.

An alternative is to change the wrapping of commands by Proof General completely, using the post-Isabelle2007 Isabelle command called 'Isabelle.command', which allows reliable nesting of commands submitted to the Isar toplevel. Of course this would break compatibility with Isabelle2005 and Isabelle2007.

[Makarius]

If you want to do anything about this for PG 4.0, I recommend the Isabelle.command solution. This is Isabelle's answer to all such synchronization problems. Another advantage is that you could pass source positions down to the system, e.g. like this:

Isabelle.command ("file" = "Foo.thy", "line" = "42") "lemma \034A ==> A\034"

The occurrences of \034 above refer to escaped double quotes; any character code can be represented like that. For robust encoding of such Isar strings the following characters should be escaped: anything in the range of 0..31 (the control block below space), and backslash, and double quote.

See also ​http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009/src/Pure/Tools/isabelle_syntax.scala#l14

[nikecitycn]

​Nike air force ones ​Air Jordan shoes ​Nike Dunks ​Nike Shox ​Nike Shoes

[David Aspinall]

This is fixed in v 10.9 of isar.el, which has an experimental command wrapping patch applied. See #199.

[deman]

​effektive fettverbrennung ​Zahnaufhellung Tipps