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

[Makarius]

A few hints on using the "error" function in Isabelle/ML properly.

The ERROR exceptions being produced here are treated by the Isar toplevel 
as "user-level error messages", i.e. are posted in clear text with certain 
markup.  This is meant for the end-user, no references to internal ML 
entities should be given here (no function names, no ML notation).

The easiest way to indicate generic program failure -- not user errors -- 
is via (raise Fail "blah").  Here the toplevel clearly indicates that this 
is a low-level exception, and also prints the source position of the ML 
raise statement.  Thus old-style messages like "foo_bar: bad argument" to 
refer to some function foo_bar are no longer necessary.

Kernel exceptions TYPE, TERM, THM also have their place in situations 
where kernel-like operations are involved.  The printing is similar as for 
Fail, although there is some special treatment when Toplevel.debug is 
enabled.


 	Makarius