# HG changeset patch # User wenzelm # Date 1287177985 -3600 # Node ID 7480a7a159cb286b04c4bd6e653298f73462336f # Parent a5a731dec31cb70b19a24a00baa9dc479ad22b6f more on "Exceptions"; diff -r a5a731dec31c -r 7480a7a159cb doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Fri Oct 15 20:36:52 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Oct 15 22:26:25 2010 +0100 @@ -265,7 +265,7 @@ *} -section {* Message output channels *} +section {* Message output channels \label{sec:message-channels} *} text {* Isabelle provides output channels for different kinds of messages: regular output, high-volume tracing information, warnings, @@ -343,4 +343,85 @@ \end{warn} *} + +section {* Exceptions *} + +text {* The Standard ML semantics of strict functional evaluation + together with exceptions is rather well defined, but some delicate + points need to be observed to avoid that ML programs go wrong + despite static type-checking. Exceptions in Isabelle/ML are + subsequently categorized as follows. + + \paragraph{Regular user errors.} These are meant to provide + informative feedback about malformed input etc. + + The \emph{error} function raises the corresponding \emph{ERROR} + exception, with a plain text message as argument. \emph{ERROR} + exceptions can be handled internally, in order to be ignored, turned + into other exceptions, or cascaded by appending messages. If the + corresponding Isabelle/Isar command terminates with an \emph{ERROR} + exception state, the toplevel will take care to print the result on + the error channel (see \secref{sec:message-channels}). + + It is considered bad style to refer to internal function names or + values in ML source notation in user error messages. + + Grammatical correctness of error messages can be improved by + \emph{omitting} final punctuation: messages are often concatenated + or put into a larger context (e.g.\ augmented with source position). + By not insisting in the final word at the origin of the error, the + system can perform its administrative tasks more easily and + robustly. + + \paragraph{Program failures.} There is a handful of standard + exceptions that indicate general failure situations, or failures of + core operations on logical entities (types, terms, theorems, + theories). + + These exceptions indicate a genuine breakdown of the program, so the + main purpose is to determine quickly what has happened where. + Traditionally, the (short) exception message would normally include + the name of an ML function, although this no longer necessary, + because the ML runtime system prints a detailed source position of + the corresponding @{verbatim raise} keyword. + + \medskip User modules can always introduce their own custom + exceptions locally, e.g.\ to organize internal failures robustly + without overlapping with existing exceptions. Exceptions that are + exposed in module signatures require extra care, though, and should + \emph{not} be introduced by default. Surprise by end-users or ML + users of a module can be often minimized by using plain errors or + one of the predefined exceptions. + + \paragraph{Interrupts.} These indicate arbitrary system events: + both the ML runtime system and the Isabelle/ML infrastructure signal + various exceptional situations by raising the special + \emph{Interrupt} exception in user code. + + This is the one and only way that physical events can intrude an + Isabelle/ML program. Such an interrupt can mean out-of-memory, + stack overflow, timeout, internal signaling of threads, or the user + producing a console interrupt manually. An Isabelle/ML program that + intercepts interrupts becomes dependent on physical effects produced + by the environment. Even worse, accidental use of exception + handling patterns that are too general will cover interrupts + unintentionally, and thus render the program semantics ill-defined. + + Note that the Interrupt exception dates back to the original SML90 + language definition. It was excluded from the SML97 version to + avoid its malign impact on ML program semantics, but without + providing a viable alternative. Isabelle/ML recovers physical + interruptibility (which an indispensable tool to implement managed + evaluation of Isar command transactions), but requires user code to + be strictly transparent wrt.\ interrupts. + + \begin{warn} + Isabelle/ML user code needs to terminate promptly on interruption, + without guessing at its meaning to the system infrastructure. + Temporary handling of interrupts for cleanup of global resources + etc.\ needs to be followed immediately by re-raising of the original + exception. + \end{warn} +*} + end \ No newline at end of file