synchronization loss with interrupts

[Alexander Krauss]

Steps to reproduce:

1. load the following script, which contains a nonterminating command:

     theory Scratch imports Main begin
   
     lemma foo: "Suc x = Suc x" ..
   
     lemma "P (Suc x)"
     apply (simp add: foo)
   

2. Go to the simp-command that does not terminate

3. Perform the following actions: Undo, Interrupt, Undo, Next

Of course there is the usual warning message telling me about possible sync losses, but I somehow got used to things being "probably ok" :-)

using cvs version as of 2009-11-24 18:12 and GNU Emacs 23.1.1

[David Aspinall]

Many thanks for the useful test case and explanation. Fixed now in proof-script 10.58: the undo is not allowed while processing is active, you get the "Proof Shell Busy" message.