# HG changeset patch
# User wenzelm
# Date 1618059363 -7200
# Node ID 08bef311d3825f79f71a266f166f6ce51e01d559
# Parent  53c148e398199b598d405f2218078f86ceb41ec1
more documentation;

diff -r 53c148e39819 -r 08bef311d382 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Sat Apr 10 14:55:50 2021 +0200
+++ b/lib/texinputs/isabellesym.sty	Sat Apr 10 14:56:03 2021 +0200
@@ -424,6 +424,8 @@
 \newcommand{\isasymcheckmark}{\isatext{\ding{51}}}  %requires pifont
 \newcommand{\isasymcrossmark}{\isatext{\ding{55}}}  %requires pifont
 \newcommand{\isactrlmarker}{\isatext{\ding{48}}}  %requires pifont
+\newcommand{\isactrltry}{\isakeywordcontrol{try}}
+\newcommand{\isactrlcan}{\isakeywordcontrol{can}}
 \newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
 \newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
 \newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
diff -r 53c148e39819 -r 08bef311d382 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sat Apr 10 14:55:50 2021 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat Apr 10 14:56:03 2021 +0200
@@ -1149,6 +1149,10 @@
   @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
+  \<^rail>\<open>
+    (@@{ML_antiquotation try} | @@{ML_antiquotation can}) embedded
+  \<close>
+
   \<^descr> \<^ML>\<open>try\<close>~\<open>f x\<close> makes the partiality of evaluating \<open>f x\<close> explicit via the
   option datatype. Interrupts are \<^emph>\<open>not\<close> handled here, i.e.\ this form serves
   as safe replacement for the \<^emph>\<open>unsafe\<close> version \<^ML_text>\<open>(SOME\<close>~\<open>f
@@ -1180,18 +1184,38 @@
 
 text %mlantiq \<open>
   \begin{matharray}{rcl}
+  @{ML_antiquotation_def "try"} & : & \<open>ML_antiquotation\<close> \\
+  @{ML_antiquotation_def "can"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "assert"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
-  \<^descr> \<open>@{assert}\<close> inlines a function \<^ML_type>\<open>bool -> unit\<close> that raises \<^ML>\<open>Fail\<close> if the argument is \<^ML>\<open>false\<close>. Due to inlining the source position of
-  failed assertions is included in the error output.
+  \<^descr> \<open>@{try}\<close> and \<open>{can}\<close> are similar to the corresponding functions, but the
+  argument is taken directly as ML expression: functional abstraction and
+  application is done implicitly.
+
+  \<^descr> \<open>@{assert}\<close> inlines a function \<^ML_type>\<open>bool -> unit\<close> that raises
+  \<^ML>\<open>Fail\<close> if the argument is \<^ML>\<open>false\<close>. Due to inlining the source
+  position of failed assertions is included in the error output.
 
   \<^descr> \<open>@{undefined}\<close> inlines \<^verbatim>\<open>raise\<close>~\<^ML>\<open>Match\<close>, i.e.\ the ML program
   behaves as in some function application of an undefined case.
 \<close>
 
 text %mlex \<open>
+  We define a total version of division: any failures are swept under the
+  carpet and mapped to a default value. Thus division-by-zero becomes 0, but
+  there could be other exceptions like overflow that produce the same result
+  (for unbounded integers this does not happen).
+\<close>
+
+ML \<open>
+  fun div_total x y = \<^try>\<open>x div y\<close> |> the_default 0;
+
+  \<^assert> (div_total 1 0 = 0);
+\<close>
+
+text \<open>
   The ML function \<^ML>\<open>undefined\<close> is defined in \<^file>\<open>~~/src/Pure/library.ML\<close>
   as follows:
 \<close>
@@ -1215,7 +1239,7 @@
 ML \<open>fun undefined _ = \<^undefined>\<close>
 
 text \<open>
-  \medskip Semantically, all forms are equivalent to a function definition
+  \<^medskip> Semantically, all forms are equivalent to a function definition
   without any clauses, but that is syntactically not allowed in ML.
 \<close>