[isabelle-dev] proper use of "error" channel
makarius at sketis.net
Mon Mar 22 23:48:02 CET 2010
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
More information about the isabelle-dev