# HG changeset patch
# User wenzelm
# Date 1287225286 -3600
# Node ID d4299b4158794cb80b94d7b465f66272c14c146f
# Parent  7480a7a159cb286b04c4bd6e653298f73462336f
more on "Exceptions";
tuned;

diff -r 7480a7a159cb -r d4299b415879 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Fri Oct 15 22:26:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sat Oct 16 11:34:46 2010 +0100
@@ -360,8 +360,8 @@
   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}).
+  exception state, the toplevel will 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.
@@ -380,18 +380,17 @@
 
   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.
+  Traditionally, the (short) exception message would 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.
+  users of a module can be often minimized by using plain user errors.
 
   \paragraph{Interrupts.}  These indicate arbitrary system events:
   both the ML runtime system and the Isabelle/ML infrastructure signal
@@ -401,11 +400,12 @@
   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.
+  producing a console interrupt manually etc.  An Isabelle/ML program
+  that intercepts interrupts becomes dependent on physical effects of
+  the environment.  Even worse, exception handling patterns that are
+  too general by accident, e.g.\ by mispelled exception constructors,
+  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
@@ -424,4 +424,45 @@
   \end{warn}
 *}
 
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
+  @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
+  @{index_ML reraise: "exn -> 'a"} \\
+  @{index_ML Exn.is_interrupt: "exn -> bool"} \\
+  @{index_ML exception_trace: "(unit -> 'a) -> 'a"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML try}~@{text "f x"} makes the partiality of evaluating
+  @{text "f x"} explicit via the option datatype.  Interrupts are
+  \emph{not} handled here, i.e.\ this form serves as safe replacement
+  for the \emph{unsafe} version @{verbatim "(SOME"}~@{text "f
+  x"}~@{verbatim "handle _ => NONE)"} that is occasionally seen in
+  books about SML.
+
+  \item @{ML can} is similar to @{ML try} with more abstract result.
+
+  \item @{ML reraise}~@{text "exn"} raises exception @{text "exn"}
+  while preserving its implicit position information (if possible,
+  depending on the ML platform).
+
+  \item @{ML Exn.is_interrupt} identifies interrupts robustly, without
+  having to mention concrete exception constructors in user code.
+  Handled interrupts need to be re-raised promptly!
+
+  \item @{ML exception_trace}~@{verbatim "(fn _ =>"}~@{text
+  "e"}@{verbatim ")"} evaluates expression @{text "e"} while printing
+  a full trace of its stack of nested exceptions (if possible,
+  depending on the ML platform).\footnote{In various versions of
+  Poly/ML the trace will appear on raw stdout of the Isabelle
+  process.}
+
+  Inserting @{ML exception_trace} into ML code temporarily is useful
+  for debugging, but not suitable for production code.
+
+  \end{description}
+*}
+
 end
\ No newline at end of file