[isabelle-dev] proper use of "error" channel
nipkow at in.tum.de
Tue Mar 23 07:35:06 CET 2010
Shouldn't this go into some documentation for future reference?
> 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
> 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.
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev