more general ML_Antiquotation.special_form;
more general "try" forms: support 'finally' or 'catch';

--- a/src/Pure/Concurrent/isabelle_thread.ML	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 16:17:43 2023 +0200
@@ -24,6 +24,8 @@
   val interrupt_exn: 'a Exn.result
   val interrupt_self: unit -> 'a
   val interrupt_other: T -> unit
+  val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
+  val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a
   val try: (unit -> 'a) -> 'a option
   val can: (unit -> 'a) -> bool
 end;
@@ -117,6 +119,12 @@
 fun interrupt_other t =
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
+fun try_catch e f =
+  e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn;
+
+fun try_finally e f =
+  Exn.release (Exn.capture e () before f ());
+
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();
 

--- a/src/Pure/ML/ml_antiquotation.ML	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Mon Sep 25 16:17:43 2023 +0200
@@ -18,7 +18,9 @@
   val inline_embedded: binding -> string context_parser -> theory -> theory
   val value: binding -> string context_parser -> theory -> theory
   val value_embedded: binding -> string context_parser -> theory -> theory
-  val special_form: binding -> string -> theory -> theory
+  val special_form: binding ->
+    (Proof.context -> Input.source -> string * ML_Lex.token Antiquote.antiquote list list) ->
+    theory -> theory
   val conditional: binding -> (Proof.context -> bool) -> theory -> theory
 end;
 
@@ -67,23 +69,31 @@
 
 (* ML macros *)
 
-fun special_form binding operator =
+fun special_form binding parse =
   ML_Context.add_antiquotation binding true
     (fn _ => fn src => fn ctxt =>
       let
-        val s = Token.read ctxt Parse.embedded_input src;
+        val input = Token.read ctxt Parse.embedded_input src;
         val tokenize = ML_Lex.tokenize_no_range;
-        val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
+        val tokenize_range = ML_Lex.tokenize_range (Input.range_of input);
+        val eq = tokenize " = ";
 
-        val (decl, ctxt') = ML_Context.read_antiquotes s ctxt;
+        val (operator, sections) = parse ctxt input;
+        val (decls, ctxt') = ML_Context.expand_antiquotes_list sections ctxt;
         fun decl' ctxt'' =
           let
-            val (ml_env, ml_body) = decl ctxt'';
+            val (sections_env, sections_body) = split_list (decls ctxt'');
+            val sections_bind =
+              sections_body |> map_index (fn (i, body) =>
+                let
+                  val name = tokenize ("expr" ^ (if i = 0 then "" else string_of_int i));
+                  val bind = if i = 0 then tokenize "val " else tokenize "and ";
+                in (bind @ name @ eq @ body, name) end);
             val ml_body' =
-              tokenize "let val expr = (fn () => " @ ml_body @ tokenize ");" @
-              tokenize " val " @ tokenize_range "result" @
-              tokenize (" = " ^ operator ^ " expr; in result end");
-          in (ml_env, ml_body') end;
+              tokenize "let " @ maps #1 sections_bind @
+              tokenize " val " @ tokenize_range "result" @ eq @
+              tokenize operator @ maps #2 sections_bind @ tokenize " in result end";
+          in (flat sections_env, ml_body') end;
       in (decl', ctxt') end);
 
 fun conditional binding check =

--- a/src/Pure/ML/ml_antiquotations.ML	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon Sep 25 16:17:43 2023 +0200
@@ -340,12 +340,68 @@
 in end;
 
 
-(* special forms for option type *)
+(* exception handling *)
+
+local
+
+val tokenize = ML_Lex.tokenize_no_range;
+val tokenize_range = ML_Lex.tokenize_range o Input.range_of;
+val tokenize_text = map Antiquote.Text o ML_Lex.tokenize_no_range;
+
+val bg_expr = tokenize_text "(fn () =>";
+val en_expr = tokenize_text ")";
+fun make_expr a = bg_expr @ a @ en_expr;
+
+val bg_handler = tokenize_text "(fn";
+val en_handler = tokenize_text "| exn => Exn.reraise exn)";
+fun make_handler a = bg_handler @ a @ en_handler;
+
+fun report_special tok = (ML_Lex.pos_of tok, Markup.keyword3);
+
+fun print_special tok =
+  let val (pos, markup) = report_special tok
+  in Markup.markup markup (ML_Lex.content_of tok) ^ Position.here pos end;
+
+val is_catch = ML_Lex.is_ident_with (fn x => x = "catch");
+val is_finally = ML_Lex.is_ident_with (fn x => x = "finally");
+fun is_special t = is_catch t orelse is_finally t;
+val is_special_text = fn Antiquote.Text t => is_special t | _ => false;
+
+fun parse_try ctxt input =
+  let
+    val ants = ML_Lex.read_source input;
+    val specials = ants
+      |> map_filter (fn Antiquote.Text t => if is_special t then SOME t else NONE | _ => NONE);
+    val _ = Context_Position.reports ctxt (map report_special specials);
+  in
+    (case specials of
+      [] => ("Isabelle_Thread.try", [make_expr ants])
+    | [s] =>
+        let val (a, b) = ants |> chop_prefix (not o is_special_text) ||> tl in
+          if is_finally s
+          then ("Isabelle_Thread.try_finally", [make_expr a, make_expr b])
+          else ("Isabelle_Thread.try_catch", [make_expr a, make_handler b])
+        end
+    | _ => error ("Too many special keywords: " ^ commas (map print_special specials)))
+  end;
+
+fun parse_can (_: Proof.context) input =
+  ("Isabelle_Thread.can", [make_expr (ML_Lex.read_source input)]);
+
+in
 
 val _ = Theory.setup
- (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "Isabelle_Thread.try" #>
-  ML_Antiquotation.special_form \<^binding>\<open>can\<close> "Isabelle_Thread.can" #>
-  ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
+  (ML_Antiquotation.special_form \<^binding>\<open>try\<close> parse_try #>
+   ML_Antiquotation.special_form \<^binding>\<open>can\<close> parse_can);
+
+end;
+
+
+
+(* special form for option type *)
+
+val _ = Theory.setup
+  (ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
     (fn _ => fn src => fn ctxt =>
       let
         val s = Token.read ctxt Parse.embedded_input src;

--- a/src/Pure/ML/ml_lex.ML	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Sep 25 16:17:43 2023 +0200
@@ -12,6 +12,7 @@
     Space | Comment of Comment.kind option | Error of string | EOF
   eqtype token
   val stopper: token Scan.stopper
+  val is_ident_with: (string -> bool) -> token -> bool
   val is_regular: token -> bool
   val is_improper: token -> bool
   val is_comment: token -> bool
@@ -110,6 +111,9 @@
 fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x)
   | is_delimiter _ = false;
 
+fun is_ident_with pred (Token (_, (Ident, x))) = pred x
+  | is_ident_with _ _ = false;
+
 fun is_regular (Token (_, (Error _, _))) = false
   | is_regular (Token (_, (EOF, _))) = false
   | is_regular _ = true;