On Tue, 23 Mar 2010, Makarius wrote:
On Tue, 23 Mar 2010, Tobias Nipkow wrote:
Makarius schrieb:
A few hints on using the "error" function in Isabelle/ML properly.
Shouldn't this go into some documentation for future reference?
I have marked it as one of the items to go into the chapter 0 about
Isabelle/ML of the Isabelle/Isar implementation manual. That part is
still to be written, or rather assembled from parts of older manuals.
In my last vacation I was pretty close to continue there, but in the end
the vacation turned out too short.
Update on this thread: my vacation in October was sufficiently long to
write this chapter 0 of the implementation manual. Now there are approx.
30 pages only about Isabelle/ML, including quite detailed explanations of
various kinds of exceptions.
The treatment of interrupts is particularly important for asynchronous
interaction model. Thread-safety is essential for parallelism, but clean
(non-)handling of interrupts is a requirement for tools to participate in
the fully asynchronous environment.
Check your tools now, if they observe the exception model of Isabelle/ML.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
