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



See the attached email by David Aspinall.

Tobias

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

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

--- Begin Message ---
Dear All,

Makarius asked me to post a note here.  If you have any issues you would 
like to see fixed in Proof General for the 3.7 release timed to coincide 
with Isabelle 2007, please report them to me via the Trac interface here:

   http://proofgeneral.inf.ed.ac.uk/trac

You can create your own account or login with a shared account I just made,

   user name: isabelledev
   password:  isabelledev

When logged in, "New Ticket" appears in the tabs.  To see a list of 
outstanding tickets to fix for this milestone, try this query:

   http://tinyurl.com/32woo4

If you're reported something to me in the past (or even recently) by 
email it would help to upload the report, I find it hard to keep track 
of emails and what has been fixed or not otherwise.

I expect to get (a little bit) of time next week to work through these.

Thanks,

  - David

_______________________________________________
Isabelle-dev mailing list
Isabelle-dev at mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

--- End Message ---


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