On Wed, 10 Nov 2010, Jasmin Christian Blanchette wrote:
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.
This might also depend on the PG version, but I did not try it out. The
versions that are currently in use are 3.7.1.1 and 4.0. The PG message
model has always been somewhat undecidable. Urgent messages sometimes
work for you, sometimes against you. I have seen situations where a
urgent message did get precedence over errors, but that caused a loss of
synchronization.
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.
Output is already "continous" in the sense that the message slot of a
running transaction is updated incrementally, without waiting for a
strange "prompt" or something. (The prompt has been abolished anyway.)
Once a transation is reset via interrupt, the behaviour is not fully
defined yet. I am already glad to get to the point where frequent
asynchronous signalling does not cause commands halt and catch fire.
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>
I have no idea, could be something like out-of-memory. Poly/ML does not
provide more details, and cannot easily do so without introducing new
challanges to user code. Right now everything is routed through the one
"Interrupt" exception.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
