[isabelle-dev] Isabelle2009 fails to handle interrupts

[Makarius]

On Mon, 17 Aug 2009, David Aspinall wrote:

> I don't believe this is PG's fault.  I can reproduce problems in tty mode. 
> With the previous version, you sent C-c C-c and it reliably interrupted and 
> printed "*** Interrupted".  With Isabelle2009 interrupts may get ignored or 
> go unreported and output and the following prompt may or may not appear.
>
> http://proofgeneral.inf.ed.ac.uk/trac/ticket/179
>
> I've added some workaround but it's not easy to tell between a busy prover 
> and one that's been interrupted and stopped sending output but is too 
> secretive to tell you about it!

What exactly did you try here?  Is this just use_thy "ParRed" with some 
erratic C-c key presses?

Anyway, the exact interrupt behaviour has always been in flux, depending 
both on changes in the various ML systems (SML/NJ, Poly/ML 4.x, Poly/ML 
5.x) and changes in the Isar toplevel.  Let's assume Poly/ML 5.2.1 for 
now, to simplify the discussion.

First of all, there are always situations where interrupts can be ignored, 
but this should not cause any messages or silent stopping of a command. In 
a sense, you can understand an external interrupt as a *hint* to some of 
the running command transactions to fail with a proper error eventually.

There is one exception: sometimes faulty ML code explicitly handles the 
internal Interrupt exception without reraising it to make it appear on the 
toplevel.  This is usually caused by the infamous "handle _" which should 
never occur in user code; the "try" and "can" combinators will do it 
properly.

Such misinterpreted interrupts might cause strange behaviour, but 
editor/toplevel state synchronization should not be lost.


 	Makarius