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