[isabelle-dev] looping continues in the background
makarius at sketis.net
Thu Jul 24 15:11:47 CEST 2014
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.
More information about the isabelle-dev