Email Gateway (Aug 18 2022 at 11:04): Email Gateway (Aug 18 2022 at 11:04):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 11:04):From: Tobias Nipkow <nipkow@in.tum.de>
See the attached email by David Aspinall.
Tobias
Peter Lammich wrote:
Email Gateway (Aug 18 2022 at 11:04):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 11:05):From: Gergely Buday <gbuday@gmail.com>
Here it is:
http://proofgeneral.inf.ed.ac.uk/trac/
Last updated: May 03 2024 at 12:27 UTC