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

[Tobias Nipkow]

Shouldn't this go into some documentation for future reference?

Tobias

Makarius schrieb:
> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev