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

[Makarius]

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.

Nonetheless I did manage to update some other parts about about basic 
context management, although in the process I was surprised how many of 
the things that I usually say to people personally are already in there. 
This indicates that our general manual situation is probably too complex 
for people to actually look there.


 	Makarius