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



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.

If this is not the right list for PG bug reports: Sorry and what is the
right way to report PG bugs ?

regards
  Peter

-- 
Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380







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