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
