On Fri, 5 Nov 2010, Makarius wrote:
Right now (96c37a685a13) the following tools limit themselves to the old
Proof General / TTY model:
Quickcheck
Nitpick
Sledgehammer
Thanks to Jasmin for addressing this for Nitpick in 36b7ed41ca9f. The
follow-up to 96c37a685a13 for Quickcheck is still missing, though.
Generally, the main point about the interrupt discipline is to allow the
system to "reset" command transaction in a clean manner. It *is* possible
to handle interrupts very briefly, to cleanup global resources etc. It is
also possible to print a final message, if that does not involve any
serious computations that take long (or forever), or could fail otherwise.
This is similar to other signal handlers in other programming
environments.
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.
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).
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
