[isabelle-dev] looping continues in the background

[Makarius]

On Mon, 10 Mar 2014, Ondřej Kunčar wrote:

> This refers to 682bba24e474.
>
> If I have a theory file that contains a method that loops (use for example 
> lemma "False" by (intro FalseE)) and if I close this file in JEdit, the 
> method presumably still loops in the background. I have to open the file 
> again and edit it to stop the looping. Is this an intended behavior? It's 
> pretty annoying.

This behaviour is a left-over from distant past, and no longer fits to 
today's quality standards of the Prover IDE.

I have refined that in Isabelle/b6256ea3b7c5, hopefully without breaking 
anything just before Isabelle2014-RC1.


 	Makarius