[isabelle-dev] Interrupts Isabelle/ML

[Jasmin Christian Blanchette]

Hi Makarius,

You wrote:

> Here is an example pattern:
> 
>  f x handle exn =>
>    if Exn.is_interrupt exn then
>      (writeln "oops"; cleanup_quickly (); reraise exn)
>    else reraise exn;
> 
> Since the transaction is officially being reset, the above message might never reach the user in the async. document model, but PG/TTY will show it nonetheless.

At least with "urgent_message", the message was immediately overwritten by the exception error, even in Proof General; so I gave up the idea on showing any message upon user interruption.

In the new interface, one could imagine seeing continual progress from diagnosis tools such as Quickcheck and Nitpick. This is something we could look into once the new interface is in place.

> Whatever is being done with interrupts, the ML code should make it immediately clear that there is no problem.  These things need to be inspected over and over again -- recently I've found again many mistakes in my own sources, and those of David Matthews (Poly/ML basis library).

I don't know if it's related, but sometimes running Mirabelle I get spontaneous "Interrupt" exceptions, which spoil the Mirabelle run. Anyway, it would be nice if the "Interrupt" had more information as argument -- e.g., did a user press Stop in Proof General, or did the Poly/ML process run out of some resource or something. Currently I just get

    *** Interrupt
    *** Exception- TOPLEVEL_ERROR raised
    Exception- TOPLEVEL_ERROR raised
    ML>

Jasmin