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

[Alexander Krauss]

Makarius wrote:
> 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.

How does the "sys_error" function fit into this picture? I have been 
using this in cases where you are suggesting to raise Fail.

Alex