[isabelle-dev] looping continues in the background

[Makarius]

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