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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
