On Thu, 24 Jul 2014, Makarius wrote:
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.
Actually, this only addresses waste of cycles due to print functions.
Regular eval transactions that are already running continue so, according
to the monotonicity principle of PIDE. To cancel that, one would require
ways to remove document nodes: it can be done manually by clearing a
buffer and closing it without saving.
If there were one more week left, there would be a chance to make that
more convenient, but it is unlikely to happen this time.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
