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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
