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
