provide ML antiquotation "if_none": non-strict version of "the_default";

--- a/NEWS	Sat Apr 22 10:22:41 2023 +0200
+++ b/NEWS	Sat Apr 22 20:55:05 2023 +0200
@@ -283,6 +283,10 @@
 
 *** ML ***
 
+* ML antiquotation \<^if_none>\<open>expr\<close> inlines a function (fn SOME x => x
+| NONE => expr); this is a non-strict version of the regular function
+"the_default". Both are particularly useful with the |> combinator.
+
 * Improved implementations and signatures of functor Table() and
 corresponding functor Set().
 

--- a/etc/symbols	Sat Apr 22 10:22:41 2023 +0200
+++ b/etc/symbols	Sat Apr 22 20:55:05 2023 +0200
@@ -506,6 +506,7 @@
 \<^if_macos>            argument: cartouche
 \<^if_windows>          argument: cartouche
 \<^if_unix>             argument: cartouche
+\<^if_none>             argument: cartouche
 \<^cite>                argument: cartouche
 \<^nocite>              argument: cartouche
 \<^citet>               argument: cartouche

--- a/lib/texinputs/isabellesym.sty	Sat Apr 22 10:22:41 2023 +0200
+++ b/lib/texinputs/isabellesym.sty	Sat Apr 22 20:55:05 2023 +0200
@@ -495,6 +495,7 @@
 \newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}}
 \newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}}
 \newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}}
+\newcommand{\isactrlifUNDERSCOREnone}{\isakeywordcontrol{if{\isacharunderscore}none}}
 
 \newcommand{\isactrlcite}{\isakeywordcontrol{cite}}
 \newcommand{\isactrlnocite}{\isakeywordcontrol{nocite}}

--- a/src/Doc/Implementation/ML.thy	Sat Apr 22 10:22:41 2023 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat Apr 22 20:55:05 2023 +0200
@@ -1495,12 +1495,52 @@
   @{define_ML the_list: "'a option -> 'a list"} \\
   @{define_ML the_default: "'a -> 'a option -> 'a"} \\
   \end{mldecls}
+
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "if_none"} & : & \<open>ML_antiquotation\<close> \\
+  \end{matharray}
+
+  \<^rail>\<open>@@{ML_antiquotation if_none} embedded\<close>
 \<close>
 
 text \<open>
   Apart from \<^ML>\<open>Option.map\<close> most other operations defined in structure
   \<^ML_structure>\<open>Option\<close> are alien to Isabelle/ML and never used. The
   operations shown above are defined in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>.
+
+  Note that the function \<^ML>\<open>the_default\<close> is strict in all of its
+  arguments, the default value is evaluated beforehand, even if not required
+  later. In contrast, the antiquotation @{ML_antiquotation "if_none"} is
+  non-strict: the given expression is only evaluated for an application to
+  \<^ML>\<open>NONE\<close>. This allows to work with exceptions like this:
+\<close>
+
+ML \<open>
+  fun div_total x y =
+    \<^try>\<open>x div y\<close> |> the_default 0;
+
+  fun div_error x y =
+    \<^try>\<open>x div y\<close> |> \<^if_none>\<open>error "Division by zero"\<close>;
+\<close>
+
+text \<open>
+  Of course, it is also possible to handle exceptions directly, without an
+  intermediate option construction:
+\<close>
+
+ML \<open>
+  fun div_total x y =
+    x div y handle Div => 0;
+
+  fun div_error x y =
+    x div y handle Div => error "Division by zero";
+\<close>
+
+text \<open>
+  The first form works better in longer chains of functional composition, with
+  combinators like \<^ML>\<open>|>\<close> or \<^ML>\<open>#>\<close> or \<^ML>\<open>o\<close>. The second form is more
+  adequate in elementary expressions: there is no need to pretend that
+  Isabelle/ML is actually a version of Haskell.
 \<close>
 
 

--- a/src/Pure/ML/ml_antiquotations.ML	Sat Apr 22 10:22:41 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Sat Apr 22 20:55:05 2023 +0200
@@ -340,11 +340,24 @@
 in end;
 
 
-(* special forms *)
+(* special forms for option type *)
 
 val _ = Theory.setup
  (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "() |> Basics.try" #>
-  ML_Antiquotation.special_form \<^binding>\<open>can\<close> "() |> Basics.can");
+  ML_Antiquotation.special_form \<^binding>\<open>can\<close> "() |> Basics.can" #>
+  ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
+    (fn _ => fn src => fn ctxt =>
+      let
+        val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt;
+        val tokenize = ML_Lex.tokenize_no_range;
+
+        val (decl, ctxt') = ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt;
+        fun decl' ctxt'' =
+          let
+            val (ml_env, ml_body) = decl ctxt'';
+            val ml_body' = tokenize "(fn SOME x => x | NONE => " @ ml_body @ tokenize ")";
+          in (ml_env, ml_body') end;
+      in (decl', ctxt') end));
 
 
 (* basic combinators *)