[isabelle-dev] proper use of "error" channel

[Makarius]

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