# HG changeset patch
# User wenzelm
# Date 1695979183 -7200
# Node ID a9ac75d397df6708d9d17c3b7e02b8aae16cd8d2
# Parent  4de5b127c124e236fe3c25366ca48c276aee0118# Parent  fc0814e9f7a8cce559891f5ba78d0dba0560b581
merged

diff -r 4de5b127c124 -r a9ac75d397df NEWS
--- a/NEWS	Wed Sep 27 13:34:15 2023 +0100
+++ b/NEWS	Fri Sep 29 11:19:43 2023 +0200
@@ -14,6 +14,26 @@
 before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.
 
 
+*** ML ***
+
+* ML antiquotation "try" provides variants of exception handling that
+avoids accidental capture of physical interrupts (which could affect ML
+semantics in unpredictable ways):
+
+  \<^try>\<open>EXPR catch HANDLER\<close>
+  \<^try>\<open>EXPR finally HANDLER\<close>
+  \<^try>\<open>EXPR\<close>
+
+See also the implementations Isabelle_Thread.try_catch / try_finally /
+try. The HANDLER always runs as uninterruptible, but the EXPR uses the
+the current thread attributes (normally interruptible). Various examples
+occur in the Isabelle sources (.ML and .thy files).
+
+* Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
+INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
+as last resort declare [[ML_catch_all]] within the theory context.
+
+
 
 New in Isabelle2023 (September 2023)
 ------------------------------------
diff -r 4de5b127c124 -r a9ac75d397df src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Doc/Implementation/ML.thy	Fri Sep 29 11:19:43 2023 +0200
@@ -1958,7 +1958,7 @@
   \begin{mldecls}
   @{define_ML_type 'a "Exn.result"} \\
   @{define_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
-  @{define_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
+  @{define_ML Exn.result: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
   @{define_ML Exn.release: "'a Exn.result -> 'a"} \\
   @{define_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
   @{define_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
@@ -1973,8 +1973,8 @@
   precautions apply to user code: interrupts must not be absorbed
   accidentally!
 
-  \<^descr> \<^ML>\<open>Exn.interruptible_capture\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but
-  interrupts are immediately re-raised as required for user code.
+  \<^descr> \<^ML>\<open>Exn.result\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but interrupts are
+  immediately re-raised as required for user code.
 
   \<^descr> \<^ML>\<open>Exn.release\<close>~\<open>result\<close> releases the original runtime result, exposing
   its regular value or raising the reified exception.
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Library/code_test.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -141,8 +141,7 @@
 fun with_debug_dir name f =
   (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
   |> Isabelle_System.make_directory
-  |> Exn.capture f
-  |> Exn.release;
+  |> f
 
 fun dynamic_value_strict ctxt t compiler =
   let
@@ -157,8 +156,7 @@
         (driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result))
       |> parse_result compiler
     fun evaluator program _ vs_ty deps =
-      Exn.interruptible_capture eval
-        (Code_Target.compilation_text ctxt target program deps true vs_ty)
+      Exn.result eval (Code_Target.compilation_text ctxt target program deps true vs_ty)
     fun postproc f = map (apsnd (Option.map (map f)))
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
@@ -313,8 +311,8 @@
     val _ = File.write driver_path driver
     val _ =
       ML_Context.eval
-        {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
-          writeln = writeln, warning = warning}
+        {environment = ML_Env.SML, redirect = false, verbose = false, catch_all = true,
+          debug = NONE, writeln = writeln, warning = warning}
         Position.none
         (ML_Lex.read_text (code, Position.file (File.symbolic_path code_path)) @
          ML_Lex.read_text (driver, Position.file (File.symbolic_path driver_path)) @
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -1150,15 +1150,17 @@
     val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
     val answer = #1 (Isabelle_System.bash_output command)
     in
-    let
-        val result = load_glpkResult resultname
-        val _ = OS.FileSys.remove lpname
-        val _ = OS.FileSys.remove resultname
-    in
-        result
-    end
-    handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
-         | exn => if Exn.is_interrupt exn then Exn.reraise exn else raise (Execute answer)
+    \<^try>\<open>
+      let
+          val result = load_glpkResult resultname
+          val _ = OS.FileSys.remove lpname
+          val _ = OS.FileSys.remove resultname
+      in
+          result
+      end
+      catch Load_cplexResult s => raise Execute ("Load_cplexResult: "^s^"\nExecute: "^answer)
+        | _ => raise Execute answer
+    \<close>
     end
 
 fun solve_cplex prog =
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Metis.thy	Fri Sep 29 11:19:43 2023 +0200
@@ -10,7 +10,10 @@
 imports ATP
 begin
 
-ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+context notes [[ML_catch_all]]
+begin
+  ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+end
 
 
 subsection \<open>Literal selection and lambda-lifting helpers\<close>
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Sep 29 11:19:43 2023 +0200
@@ -157,21 +157,23 @@
          (Global_Theory.all_thms_of thy true)
 
 fun check_formulas tsp =
-  let
-    fun is_type_actually_monotonic T =
-      Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
-    val free_Ts = fold Term.add_tfrees ((op @) tsp) [] |> map TFree
-    val (mono_free_Ts, nonmono_free_Ts) =
-      Timeout.apply mono_timeout
-          (List.partition is_type_actually_monotonic) free_Ts
-  in
-    if not (null mono_free_Ts) then "MONO"
-    else if not (null nonmono_free_Ts) then "NONMONO"
-    else "NIX"
-  end
-  handle Timeout.TIMEOUT _ => "TIMEOUT"
-       | NOT_SUPPORTED _ => "UNSUP"
-       | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
+  \<^try>\<open>
+    let
+      fun is_type_actually_monotonic T =
+        Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
+      val free_Ts = fold Term.add_tfrees ((op @) tsp) [] |> map TFree
+      val (mono_free_Ts, nonmono_free_Ts) =
+        Timeout.apply mono_timeout
+            (List.partition is_type_actually_monotonic) free_Ts
+    in
+      if not (null mono_free_Ts) then "MONO"
+      else if not (null nonmono_free_Ts) then "NONMONO"
+      else "NIX"
+    end
+    catch Timeout.TIMEOUT _ => "TIMEOUT"
+      | NOT_SUPPORTED _ => "UNSUP"
+      | _ => "UNKNOWN"
+  \<close>
 
 fun check_theory thy =
   let
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Sep 29 11:19:43 2023 +0200
@@ -75,6 +75,11 @@
   tptp_informative_failure = true
 ]]
 
+ML \<open>
+exception UNSUPPORTED_ROLE
+exception INTERPRET_INFERENCE
+\<close>
+
 ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close>
 ML "open TPTP_Reconstruct_Library"
 ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close>
@@ -867,16 +872,18 @@
           SOME (rev acc)
         else NONE
       else
-        let
-          val (arg_ty, val_ty) = Term.dest_funT cur_ty
-          (*now find a param of type arg_ty*)
-          val (candidate_param, params') =
-            find_and_remove (snd #> pair arg_ty #> (op =)) params
-        in
-          use_candidate target_ty params' (candidate_param :: acc) val_ty
-        end
-        handle TYPE ("dest_funT", _, _) => NONE  (* FIXME fragile *)
+        \<^try>\<open>
+          let
+            val (arg_ty, val_ty) = Term.dest_funT cur_ty
+            (*now find a param of type arg_ty*)
+            val (candidate_param, params') =
+              find_and_remove (snd #> pair arg_ty #> (op =)) params
+          in
+            use_candidate target_ty params' (candidate_param :: acc) val_ty
+          end
+          catch TYPE ("dest_funT", _, _) => NONE  (* FIXME fragile *)
              | _ => NONE  (* FIXME avoid catch-all handler *)
+        \<close>
 
     val (skolem_const_ty, params') = skolem_const_info_of conclusion
 
@@ -2012,9 +2019,6 @@
 subsection "Leo2 reconstruction tactic"
 
 ML \<open>
-exception UNSUPPORTED_ROLE
-exception INTERPRET_INFERENCE
-
 (*Failure reports can be adjusted to avoid interrupting
   an overall reconstruction process*)
 fun fail ctxt x =
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/TPTP/TPTP_Test.thy
--- a/src/HOL/TPTP/TPTP_Test.thy	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy	Fri Sep 29 11:19:43 2023 +0200
@@ -56,15 +56,11 @@
     let
       val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
     in
-     (f file_name; ())
+     \<^try>\<open>(f file_name; ()) catch exn =>
      (*otherwise report exceptions as warnings*)
-     handle exn =>
-       if Exn.is_interrupt exn then
-         Exn.reraise exn
-       else
-         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
-          " raised exception: " ^ Runtime.exn_message exn);
-          default_val)
+       (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
+        " raised exception: " ^ Runtime.exn_message exn);
+        default_val)\<close>
     end
 
   fun timed_test ctxt f test_files =
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -95,9 +95,7 @@
   | exn => "exception: " ^ General.exnMessage exn);
 
 fun run_action_function f =
-  f () handle exn =>
-    if Exn.is_interrupt exn then Exn.reraise exn
-    else print_exn exn;
+  \<^try>\<open>f () catch exn => print_exn exn\<close>;
 
 fun make_action_path ({index, label, name, ...} : action_context) =
   Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -273,31 +273,32 @@
 local
 
 fun run_sh params keep pos state =
-  let
-    fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
-        let
-          val filename = "prob_" ^
-            StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
-            StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
-        in
-          Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
-          #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
-          #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
-          #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
-        end
-      | set_file_name NONE = I
-    val state' = state
-      |> Proof.map_context (set_file_name keep)
+  \<^try>\<open>
+    let
+      fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
+          let
+            val filename = "prob_" ^
+              StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
+              StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
+          in
+            Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
+            #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
+            #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
+            #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
+          end
+        | set_file_name NONE = I
+      val state' = state
+        |> Proof.map_context (set_file_name keep)
 
-    val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
-      Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
-        Sledgehammer_Fact.no_fact_override state') ()
-  in
-    (sledgehammer_outcome, msg, cpu_time)
-  end
-  handle
-    ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
-  | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
+      val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
+        Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
+          Sledgehammer_Fact.no_fact_override state') ()
+    in
+      (sledgehammer_outcome, msg, cpu_time)
+    end
+    catch ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
+      | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
+  \<close>
 
 in
 
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -1006,23 +1006,25 @@
                 if overlord then ()
                 else List.app (ignore o try File.rm) [kki_path, out_path, err_path]
             in
-              let
-                val _ = File.write kki_path kki
-                val rc =
-                  Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
-                    \\"$KODKODI/bin/kodkodi\"" ^
-                    (" -max-msecs " ^ string_of_int timeout) ^
-                    (if solve_all then " -solve-all" else "") ^
-                    " -max-solutions " ^ string_of_int max_solutions ^
-                    (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
-                    " < " ^ File.bash_path kki_path ^
-                    " > " ^ File.bash_path out_path ^
-                    " 2> " ^ File.bash_path err_path)
-                val out = File.read out_path
-                val err = File.read err_path
-                val _ = remove_temporary_files ()
-              in (rc, out, err) end
-              handle exn => (remove_temporary_files (); Exn.reraise exn)
+              \<^try>\<open>
+                let
+                  val _ = File.write kki_path kki
+                  val rc =
+                    Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
+                      \\"$KODKODI/bin/kodkodi\"" ^
+                      (" -max-msecs " ^ string_of_int timeout) ^
+                      (if solve_all then " -solve-all" else "") ^
+                      " -max-solutions " ^ string_of_int max_solutions ^
+                      (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
+                      " < " ^ File.bash_path kki_path ^
+                      " > " ^ File.bash_path out_path ^
+                      " 2> " ^ File.bash_path err_path)
+                  val out = File.read out_path
+                  val err = File.read err_path
+                  val _ = remove_temporary_files ()
+                in (rc, out, err) end
+                finally remove_temporary_files ()
+              \<close>
             end
           else
             (timeout, (solve_all, (max_solutions, (max_threads, kki))))
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -211,8 +211,7 @@
 fun with_overlord_dir name f =
   (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
   |> Isabelle_System.make_directory
-  |> Exn.capture f
-  |> Exn.release
+  |> f
 
 fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
     ctxt cookie (code_modules_bytes, _) =
@@ -315,7 +314,7 @@
 fun dynamic_value_strict opts cookie ctxt postproc t =
   let
     fun evaluator program _ vs_ty_t deps =
-      Exn.interruptible_capture (value opts ctxt cookie)
+      Exn.result (value opts ctxt cookie)
         (Code_Target.compilation_text ctxt target program deps true vs_ty_t)
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -328,12 +328,9 @@
       if debug then
         really_go ()
       else
-        (really_go ()
-         handle
-           ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
-         | exn =>
-           if Exn.is_interrupt exn then Exn.reraise exn
-           else (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n"))
+        \<^try>\<open>really_go ()
+          catch ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
+            | exn => (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n")\<close>
 
     val (outcome, message) = Timeout.apply hard_timeout go ()
     val () = check_expected_outcome ctxt prover_name expect outcome
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -578,20 +578,17 @@
   handle Symtab.DUP _ => accum (* robustness (in case the state file violates the invariant) *)
 
 fun try_graph ctxt when def f =
-  f ()
-  handle
-    Graph.CYCLES (cycle :: _) =>
-    (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
-  | Graph.DUP name =>
-    (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
-  | Graph.UNDEF name =>
-    (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
-  | exn =>
-    if Exn.is_interrupt exn then
-      Exn.reraise exn
-    else
-      (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
-       def)
+  \<^try>\<open>f ()
+    catch
+      Graph.CYCLES (cycle :: _) =>
+      (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
+    | Graph.DUP name =>
+      (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
+    | Graph.UNDEF name =>
+      (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
+    | exn =>
+        (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
+         def)\<close>
 
 fun graph_info G =
   string_of_int (length (Graph.keys G)) ^ " node(s), " ^
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -279,7 +279,7 @@
          (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof,
           atp_abduce_candidates, outcome),
          (format, type_enc)) =
-      with_cleanup clean_up run () |> tap export
+      \<^try>\<open>run () finally clean_up ()\<close> |> tap export
 
     val (outcome, used_facts, preferred_methss, message) =
       (case outcome of
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -104,13 +104,10 @@
     val birth = Timer.checkRealTimer timer
 
     val filter_result as {outcome, ...} =
-      SMT_Solver.smt_filter ctxt goal facts i run_timeout options
-      handle exn =>
-      if Exn.is_interrupt exn orelse debug then
-        Exn.reraise exn
-      else
-        {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
-         atp_proof = K []}
+      \<^try>\<open>SMT_Solver.smt_filter ctxt goal facts i run_timeout options
+        catch exn =>
+          {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE,
+           atp_proof = K []}\<close>
 
     val death = Timer.checkRealTimer timer
     val run_time = death - birth
diff -r 4de5b127c124 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -12,7 +12,6 @@
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
-  val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time : string -> string -> Time.time
   val subgoal_count : Proof.state -> int
@@ -42,11 +41,6 @@
 val serial_commas = Try.serial_commas
 val simplify_spaces = strip_spaces false (K true)
 
-fun with_cleanup clean_up f x =
-  Exn.capture f x
-  |> tap (fn _ => clean_up x)
-  |> Exn.release
-
 fun parse_bool_option option name s =
   (case s of
      "smart" => if option then NONE else raise Option.Option
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -134,14 +134,14 @@
       manager_loop);
 
 fun shutdown () =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
       if is_shutdown Normal st then (false, st)
       else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
         raise Fail "Concurrent attempt to shutdown event timer"
       else (true, make_state (requests, Shutdown_Req, manager_check manager)))
     then
-      restore_attributes (fn () =>
+      run (fn () =>
         Synchronized.guarded_access state
           (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) ()
       handle exn =>
@@ -149,7 +149,7 @@
           Synchronized.change state (fn State {requests, manager, ...} =>
             make_state (requests, Normal, manager))
         else ()
-    else ()) ();
+    else ());
 
 
 (* main operations *)
@@ -170,12 +170,12 @@
     in (canceled, make_state (requests', status, manager')) end);
 
 fun future physical time =
-  Thread_Attributes.uninterruptible (fn _ => fn () =>
+  Thread_Attributes.uninterruptible_body (fn _ =>
     let
       val req: request Single_Assignment.var = Single_Assignment.var "req";
       fun abort () = ignore (cancel (Single_Assignment.await req));
       val promise: unit future = Future.promise_name "event_timer" abort;
       val _ = Single_Assignment.assign req (request physical time (Future.fulfill promise));
-    in promise end) ();
+    in promise end);
 
 end;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -214,7 +214,7 @@
      then Thread_Attributes.private_interrupts
      else Thread_Attributes.public_interrupts)
     (fn _ => f x)
-  before Thread_Attributes.expose_interrupt ();
+  before Isabelle_Thread.expose_interrupt ();
 
 
 (* worker threads *)
@@ -234,7 +234,7 @@
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
-        val test = Exn.capture Thread_Attributes.expose_interrupt ();
+        val test = Isabelle_Thread.expose_interrupt_result ();
         val _ =
           if ok andalso not (Exn.is_interrupt_exn test) then ()
           else if null (cancel_now group) then ()
@@ -550,7 +550,7 @@
 (* forked results: nested parallel evaluation *)
 
 fun forked_results {name, deps} es =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       val (group, pri) =
         (case worker_task () of
@@ -560,9 +560,9 @@
       val futures =
         forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
     in
-      restore_attributes join_results futures
+      run join_results futures
         handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
-    end) ();
+    end);
 
 
 (* task context for running thread *)
@@ -614,10 +614,10 @@
 
 fun cond_forks args es =
   if enabled () then forks args es
-  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
+  else map (fn e => value_result (Exn.result e ())) es;
 
 fun map_future f x =
-  if is_finished x then value_result (Exn.interruptible_capture (f o join) x)
+  if is_finished x then value_result (Exn.result (f o join) x)
   else
     let
       val task = task_of x;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -14,6 +14,7 @@
   val print: T -> string
   val self: unit -> T
   val is_self: T -> bool
+  val threads_stack_limit: real Unsynchronized.ref
   val stack_limit: unit -> int option
   type params = {name: string, stack_limit: int option, interrupts: bool}
   val attributes: params -> Thread.Thread.threadAttribute list
@@ -24,6 +25,11 @@
   val interrupt_exn: 'a Exn.result
   val interrupt_self: unit -> 'a
   val interrupt_other: T -> unit
+  structure Exn: EXN
+  val expose_interrupt_result: unit -> unit Exn.result
+  val expose_interrupt: unit -> unit  (*exception Interrupt*)
+  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;
@@ -43,11 +49,11 @@
 val get_name = #name o dest;
 val get_id = #id o dest;
 
-val equal = Thread.Thread.equal o apply2 get_thread;
+fun equal (t1, t2) = Thread.Thread.equal (get_thread t1, get_thread t2);
 
 fun print t =
   (case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^
-    "-" ^ string_of_int (get_id t);
+    "-" ^ Int.toString (get_id t);
 
 
 (* self *)
@@ -73,11 +79,12 @@
 
 (* fork *)
 
+val threads_stack_limit = Unsynchronized.ref 0.25;
+
 fun stack_limit () =
   let
-    val threads_stack_limit =
-      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
-  in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end;
+    val limit = Real.floor (! threads_stack_limit * 1024.0 * 1024.0 * 1024.0);
+  in if limit <= 0 then NONE else SOME limit end;
 
 type params = {name: string, stack_limit: int option, interrupts: bool};
 
@@ -117,7 +124,33 @@
 fun interrupt_other t =
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
+structure Exn: EXN =
+struct
+  open Exn;
+  val capture = capture0;
+end;
+
+fun expose_interrupt_result () =
+  let
+    val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ());
+    val _ = Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
+    val test = Exn.capture Thread.Thread.testInterrupt ();
+    val _ = Thread_Attributes.set_attributes orig_atts;
+  in test end;
+
+val expose_interrupt = Exn.release o expose_interrupt_result;
+
+fun try_catch e f =
+  Thread_Attributes.uninterruptible_body (fn run =>
+    run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn);
+
+fun try_finally e f =
+  Thread_Attributes.uninterruptible_body (fn run =>
+    Exn.release (Exn.capture (run e) () before f ()));
+
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();
 
 end;
+
+structure Exn = Isabelle_Thread.Exn;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -85,7 +85,7 @@
       (case peek (Lazy var) of
         SOME res => res
       | NONE =>
-          Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+          Thread_Attributes.uninterruptible_body (fn run =>
             let
               val (expr, x) =
                 Synchronized.change_result var
@@ -101,7 +101,7 @@
               (case expr of
                 SOME (name, e) =>
                   let
-                    val res0 = Exn.capture (restore_attributes e) ();
+                    val res0 = Exn.capture (run e) ();
                     val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
                     val res = Future.get_result x;
                     val _ =
@@ -114,8 +114,8 @@
                         interrupt, until there is a fresh start*)
                       else Synchronized.change var (fn _ => Expr (name, e));
                   in res end
-              | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
-            end) ());
+              | NONE => Exn.capture (run (fn () => Future.join x)) ())
+            end));
 
 end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/multithreading.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -67,9 +67,9 @@
 
 fun tracing level msg =
   if ! trace < level then ()
-  else Thread_Attributes.uninterruptible (fn _ => fn () =>
+  else Thread_Attributes.uninterruptible_body (fn _ =>
     (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
-      handle _ (*sic*) => ()) ();
+      handle _ (*sic*) => ());
 
 fun tracing_time detailed time =
   tracing
@@ -83,7 +83,7 @@
 (* synchronized evaluation *)
 
 fun synchronized name lock e =
-  Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Exn.release (Thread_Attributes.uninterruptible_body (fn run =>
     if ! trace > 0 then
       let
         val immediate =
@@ -96,15 +96,15 @@
               val time = Timer.checkRealTimer timer;
               val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
             in false end;
-        val result = Exn.capture (restore_attributes e) ();
+        val result = Exn.capture0 (run e) ();
         val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
         val _ = Thread.Mutex.unlock lock;
       in result end
     else
       let
         val _ = Thread.Mutex.lock lock;
-        val result = Exn.capture (restore_attributes e) ();
+        val result = Exn.capture0 (run e) ();
         val _ = Thread.Mutex.unlock lock;
-      in result end) ());
+      in result end));
 
 end;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -37,7 +37,7 @@
 
 fun map' params f xs = Par_Exn.release_first (managed_results params f xs);
 fun map f = map' {name = "", sequential = false} f;
-fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
+fun map_independent f = map (Exn.result f) #> Par_Exn.release_all;
 
 fun get_some f xs =
   let
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/single_assignment.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -61,9 +61,9 @@
         (case ! state of
           Set _ => assign_fail name
         | Unset _ =>
-            Thread_Attributes.uninterruptible (fn _ => fn () =>
+            Thread_Attributes.uninterruptible_body (fn _ =>
              (state := Set x; RunCall.clearMutableBit state;
-               Thread.ConditionVar.broadcast cond)) ())));
+               Thread.ConditionVar.broadcast cond)))));
 
 end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -57,9 +57,9 @@
         (case ! state of
           Immutable _ => immutable_fail name
         | Mutable _ =>
-            Thread_Attributes.uninterruptible (fn _ => fn () =>
+            Thread_Attributes.uninterruptible_body (fn _ =>
              (state := Immutable x; RunCall.clearMutableBit state;
-               Thread.ConditionVar.broadcast cond)) ())));
+               Thread.ConditionVar.broadcast cond)))));
 
 
 (* synchronized access *)
@@ -81,9 +81,9 @@
                     | Exn.Res false => NONE
                     | Exn.Exn exn => Exn.reraise exn)
                 | SOME (y, x') =>
-                    Thread_Attributes.uninterruptible (fn _ => fn () =>
+                    Thread_Attributes.uninterruptible_body (fn _ =>
                       (state := Mutable {lock = lock, cond = cond, content = x'};
-                        Thread.ConditionVar.broadcast cond; SOME y)) ()));
+                        Thread.ConditionVar.broadcast cond; SOME y))));
         in try_change () end));
 
 fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -156,13 +156,13 @@
 fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
 
 fun update_timing update (Task {timing, ...}) e =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       val start = Time.now ();
-      val result = Exn.capture (restore_attributes e) ();
+      val result = Exn.capture (run e) ();
       val t = Time.now () - start;
       val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
-    in Exn.release result end) ();
+    in Exn.release result end);
 
 fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
   prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/thread_attributes.ML
--- a/src/Pure/Concurrent/thread_attributes.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/thread_attributes.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -18,7 +18,7 @@
   val safe_interrupts: attributes -> attributes
   val with_attributes: attributes -> (attributes -> 'a) -> 'a
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  val expose_interrupt: unit -> unit  (*exception Interrupt*)
+  val uninterruptible_body: ((('b -> 'c) -> 'b -> 'c) -> 'a) -> 'a
 end;
 
 structure Thread_Attributes: THREAD_ATTRIBUTES =
@@ -96,7 +96,7 @@
     if atts1 = atts2 then e atts1
     else
       let
-        val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) ();
+        val result = Exn.capture0 (fn () => (set_attributes atts2; e atts1)) ();
         val _ = set_attributes atts1;
       in Exn.release result end
   end;
@@ -107,12 +107,7 @@
   with_attributes no_interrupts (fn atts =>
     f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
 
-fun expose_interrupt () =
-  let
-    val orig_atts = safe_interrupts (get_attributes ());
-    val _ = set_attributes test_interrupts;
-    val test = Exn.capture Thread.Thread.testInterrupt ();
-    val _ = set_attributes orig_atts;
-  in Exn.release test end;
+fun uninterruptible_body body =
+  uninterruptible (fn run => fn () => body run) ();
 
 end;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/thread_data.ML
--- a/src/Pure/Concurrent/thread_data.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/thread_data.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -30,13 +30,13 @@
 fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
 
 fun setmp v data f x =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       val orig_data = get v;
       val _ = put v data;
-      val result = Exn.capture (restore_attributes f) x;
+      val result = Exn.capture0 (run f) x;
       val _ = put v orig_data;
-    in Exn.release result end) ();
+    in Exn.release result end);
 
 end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/thread_data_virtual.ML
--- a/src/Pure/Concurrent/thread_data_virtual.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/thread_data_virtual.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -30,13 +30,13 @@
     | SOME x => Inttab.update (i, Universal.tagInject tag x));
 
 fun setmp v data f x =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       val orig_data = get v;
       val _ = put v data;
-      val result = Exn.capture (restore_attributes f) x;
+      val result = Exn.capture (run f) x;
       val _ = put v orig_data;
-    in Exn.release result end) ();
+    in Exn.release result end);
 
 end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/timeout.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -46,7 +46,7 @@
 
         val stop = Time.now ();
         val was_timeout = not (Event_Timer.cancel request);
-        val test = Exn.capture Thread_Attributes.expose_interrupt ();
+        val test = Isabelle_Thread.expose_interrupt_result ();
       in
         if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
         then raise TIMEOUT (stop - start)
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Concurrent/unsynchronized.ML
--- a/src/Pure/Concurrent/unsynchronized.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Concurrent/unsynchronized.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -39,13 +39,13 @@
 fun add i n = (i := ! i + (n: int); ! i);
 
 fun setmp flag value f x =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       val orig_value = ! flag;
       val _ = flag := value;
-      val result = Exn.capture (restore_attributes f) x;
+      val result = Exn.capture0 (run f) x;
       val _ = flag := orig_value;
-    in Exn.release result end) ();
+    in Exn.release result end);
 
 
 (* weak references *)
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/exn.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -11,7 +11,7 @@
   val cat_error: string -> string -> 'a
 end;
 
-signature EXN =
+signature EXN0 =
 sig
   include BASIC_EXN
   val polyml_location: exn -> PolyML.location option
@@ -21,7 +21,7 @@
   val is_exn: 'a result -> bool
   val get_res: 'a result -> 'a option
   val get_exn: 'a result -> exn option
-  val capture: ('a -> 'b) -> 'a -> 'b result
+  val capture0: ('a -> 'b) -> 'a -> 'b result  (*unmanaged interrupts*)
   val release: 'a result -> 'a
   val map_res: ('a -> 'b) -> 'a result -> 'b result
   val maps_res: ('a -> 'b result) -> 'a result -> 'b result
@@ -29,13 +29,19 @@
   val cause: exn -> exn
   val is_interrupt: exn -> bool
   val is_interrupt_exn: 'a result -> bool
-  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val result: ('a -> 'b) -> 'a -> 'b result
   val failure_rc: exn -> int
   exception EXCEPTIONS of exn list
   val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
 end;
 
-structure Exn: EXN =
+signature EXN =
+sig
+  include EXN0
+  val capture: ('a -> 'b) -> 'a -> 'b result  (*managed interrupts*)
+end;
+
+structure Exn: EXN0 =
 struct
 
 (* location *)
@@ -74,7 +80,7 @@
 fun get_exn (Exn exn) = SOME exn
   | get_exn _ = NONE;
 
-fun capture f x = Res (f x) handle e => Exn e;
+fun capture0 f x = Res (f x) handle e => Exn e;
 
 fun release (Res y) = y
   | release (Exn e) = reraise e;
@@ -101,7 +107,7 @@
 fun is_interrupt_exn (Exn exn) = is_interrupt exn
   | is_interrupt_exn _ = false;
 
-fun interruptible_capture f x =
+fun result f x =
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 fun failure_rc exn = if is_interrupt exn then 130 else 2;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/exn.scala	Fri Sep 29 11:19:43 2023 +0200
@@ -93,7 +93,7 @@
       case _ => false
     }
 
-  def interruptible_capture[A](e: => A): Result[A] =
+  def result[A](e: => A): Result[A] =
     try { Res(e) }
     catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/General/file_stream.ML
--- a/src/Pure/General/file_stream.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/file_stream.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -27,11 +27,12 @@
 val platform_path = ML_System.platform_path o Path.implode o Path.expand;
 
 fun with_file open_file close_file f =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
+  Thread_Attributes.uninterruptible (fn run => fn path =>
     let
       val file = open_file path;
-      val result = Exn.capture (restore_attributes f) file;
-    in close_file file; Exn.release result end);
+      val result = Exn.capture (run f) file;
+      val _ = close_file file;
+    in Exn.release result end);
 
 in
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/same.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -13,7 +13,6 @@
   val same: ('a, 'b) function
   val commit: 'a operation -> 'a -> 'a
   val function: ('a -> 'b option) -> ('a, 'b) function
-  val capture: ('a, 'b) function -> 'a -> 'b option
   val map: 'a operation -> 'a list operation
   val map_option: ('a, 'b) function -> ('a option, 'b option) function
 end;
@@ -29,8 +28,6 @@
 fun same _ = raise SAME;
 fun commit f x = f x handle SAME => x;
 
-fun capture f x = SOME (f x) handle SAME => NONE;
-
 fun function f x =
   (case f x of
     NONE => raise SAME
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/sha1.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -155,12 +155,12 @@
       (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer);
 
 fun with_memory n =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
+  Thread_Attributes.uninterruptible (fn run => fn f =>
     let
       val mem = Foreign.Memory.malloc (Word.fromInt n);
-      val res = Exn.capture (restore_attributes f) mem;
+      val result = Exn.capture (run f) mem;
       val _ = Foreign.Memory.free mem;
-    in Exn.release res end);
+    in Exn.release result end);
 
 
 (* digesting *)
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/socket_io.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -88,11 +88,13 @@
   handle OS.SysErr (msg, _) => error (msg ^ ": failed to open socket " ^ socket_name);
 
 fun with_streams f =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn socket_name =>
+  Thread_Attributes.uninterruptible (fn run => fn socket_name =>
     let
       val streams = open_streams socket_name;
-      val result = Exn.capture (restore_attributes f) streams;
-    in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end);
+      val result = Exn.capture (run f) streams;
+      val _ = BinIO.closeIn (#1 streams);
+      val _ = BinIO.closeOut (#2 streams);
+    in Exn.release result end);
 
 fun with_streams' f socket_name password =
   with_streams (fn streams =>
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/General/timing.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -90,7 +90,7 @@
 fun cond_timeit enabled msg e =
   if enabled then
     let
-      val (t, result) = timing (Exn.interruptible_capture e) ();
+      val (t, result) = timing (Exn.result e) ();
       val _ =
         if is_relevant t then
           let val end_msg = message t
@@ -111,7 +111,7 @@
 
 fun protocol name pos f x =
   let
-    val (t, result) = timing (Exn.interruptible_capture f) x;
+    val (t, result) = timing (Exn.result f) x;
     val _ = protocol_message name pos t;
   in Exn.release result end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -613,6 +613,7 @@
   register_config_string ML_Env.ML_environment #>
   register_config_bool ML_Env.ML_read_global #>
   register_config_bool ML_Env.ML_write_global #>
+  register_config_bool ML_Compiler.ML_catch_all #>
   register_config_bool ML_Options.source_trace #>
   register_config_bool ML_Options.exception_trace #>
   register_config_bool ML_Options.exception_debugger #>
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -1259,7 +1259,7 @@
     val test_proof =
       local_skip_proof true
       |> Unsynchronized.setmp testing true
-      |> Exn.interruptible_capture;
+      |> Exn.result;
 
     fun after_qed' (result_ctxt, results) state' = state'
       |> refine_goals print_rule result_ctxt (flat results)
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -331,8 +331,9 @@
 in
 
 fun apply_capture int name markers trans state =
-  (apply_body int trans state |> apply_markers name markers)
-    handle exn => (state, SOME exn);
+  (case Exn.capture (fn () => apply_body int trans state |> apply_markers name markers) () of
+    Exn.Res res => res
+  | Exn.Exn exn => (state, SOME exn));
 
 end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/exn_debugger.ML
--- a/src/Pure/ML/exn_debugger.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/exn_debugger.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -42,10 +42,10 @@
 in
 
 fun capture_exception_trace e =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       val _ = start_trace ();
-      val result = Exn.interruptible_capture (restore_attributes e) ();
+      val result = Exn.result (run e) ();
       val trace = stop_trace ();
       val trace' =
         (case result of
@@ -54,7 +54,7 @@
             trace
             |> map_filter (fn (entry, e) => if eq_exn (exn, e) then SOME entry else NONE)
             |> rev);
-    in (trace', result) end) ();
+    in (trace', result) end);
 
 end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/exn_properties.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -63,8 +63,8 @@
             startLine = #startLine loc, endLine = #endLine loc,
             startPosition = #startPosition loc, endPosition = #endPosition loc};
       in
-        Thread_Attributes.uninterruptible (fn _ => fn () =>
-          PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
+        Thread_Attributes.uninterruptible_body (fn _ =>
+          PolyML.raiseWithLocation (exn, loc') handle exn' => exn')
       end
   end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Sep 29 11:19: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 =
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -340,12 +340,67 @@
 in end;
 
 
-(* special forms for option type *)
+(* exception handling *)
+
+local
+
+val tokenize_text = map Antiquote.Text o ML_Lex.tokenize_no_range;
+val tokenize_range_text = map Antiquote.Text oo ML_Lex.tokenize_range;
+
+val bg_expr = tokenize_text "(fn () =>";
+val en_expr = tokenize_text ")";
+fun make_expr a = bg_expr @ a @ en_expr;
+
+fun make_handler range a =
+  tokenize_range_text range "(fn" @ a @
+  tokenize_range_text range "| exn => Exn.reraise exn)";
+
+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 (ML_Lex.range_of s) 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;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -7,11 +7,12 @@
 signature ML_COMPILER =
 sig
   type flags =
-    {environment: string, redirect: bool, verbose: bool,
+    {environment: string, redirect: bool, verbose: bool, catch_all: bool,
       debug: bool option, writeln: string -> unit, warning: string -> unit}
   val debug_flags: bool option -> flags
   val flags: flags
   val verbose: bool -> flags -> flags
+  val ML_catch_all: bool Config.T
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
 end;
 
@@ -21,18 +22,18 @@
 (* flags *)
 
 type flags =
-  {environment: string, redirect: bool, verbose: bool,
+  {environment: string, redirect: bool, verbose: bool, catch_all: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 fun debug_flags opt_debug : flags =
-  {environment = "", redirect = false, verbose = false,
+  {environment = "", redirect = false, verbose = false, catch_all = false,
     debug = opt_debug, writeln = writeln, warning = warning};
 
 val flags = debug_flags NONE;
 
-fun verbose b (flags: flags) =
-  {environment = #environment flags, redirect = #redirect flags, verbose = b,
-    debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+fun verbose b ({environment, redirect, verbose = _, catch_all, debug, writeln, warning}: flags) =
+  {environment = environment, redirect = redirect, verbose = b, catch_all = catch_all,
+    debug = debug, writeln = writeln, warning = warning};
 
 
 (* parse trees *)
@@ -147,6 +148,8 @@
 
 (* eval ML source tokens *)
 
+val ML_catch_all = Config.declare_bool ("ML_catch_all", \<^here>) (K false);
+
 fun eval (flags: flags) pos toks =
   let
     val opt_context = Context.get_generic_context ();
@@ -201,16 +204,29 @@
 
     val error_buffer = Unsynchronized.ref Buffer.empty;
     fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
-    fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
-    fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
+
+    fun expose_error verbose =
+      let
+        val msg = Buffer.content (! error_buffer);
+        val is_err = msg <> "";
+        val _ = if is_err orelse verbose then (output_warnings (); output_writeln ()) else ();
+      in if is_err then error (trim_line msg) else () end;
 
     fun message {message = msg, hard, location = loc, context = _} =
       let
         val pos = Exn_Properties.position_of_polyml_location loc;
-        val txt =
-          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
-          Pretty.string_of (Pretty.from_polyml msg);
-      in if hard then err txt else warn txt end;
+        val s = Pretty.string_of (Pretty.from_polyml msg);
+        val catch_all =
+          #catch_all flags orelse
+            (case opt_context of
+              NONE => false
+            | SOME context => Config.get_generic context ML_catch_all);
+        val is_err =
+          hard orelse
+            (not catch_all andalso
+              String.isPrefix "Handler catches all exceptions" (XML.content_of (YXML.parse_body s)));
+        val txt = (if is_err then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ s;
+      in if is_err then err txt else warn txt end;
 
 
     (* results *)
@@ -294,12 +310,8 @@
                 STATIC_ERRORS () => ""
               | Runtime.TOPLEVEL_ERROR => ""
               | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
-            val _ = output_warnings ();
-            val _ = output_writeln ();
-          in raise_error exn_msg end;
-  in
-    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
-    else ()
-  end;
+            val _ = err exn_msg;
+          in expose_error true end;
+  in expose_error (#verbose flags) end;
 
 end;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_compiler0.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -117,11 +117,12 @@
 
 end;
 
-fun ML_file context {verbose, debug} file =
+fun ML_file context {verbose, debug} file = Thread_Attributes.uninterruptible_body (fn run =>
   let
     val instream = TextIO.openIn file;
-    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in ML context {line = 1, file = file, verbose = verbose, debug = debug} text end;
+    val result = Exn.capture (run TextIO.inputAll) instream;
+    val _ = TextIO.closeIn instream;
+  in ML context {line = 1, file = file, verbose = verbose, debug = debug} (Exn.release result) end);
 
 fun ML_file_operations (f: bool option -> string -> unit) =
   {ML_file = f NONE, ML_file_debug = f (SOME true), ML_file_no_debug = f (SOME false)};
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_context.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -238,3 +238,4 @@
 end;
 
 val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags);
+val ML_command = ML_Context.eval_source ML_Compiler.flags;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_file.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -6,7 +6,7 @@
 
 signature ML_FILE =
 sig
-  val command: string -> bool option -> (theory -> Token.file) ->
+  val command: string -> bool -> bool option -> (theory -> Token.file) ->
     Toplevel.transition -> Toplevel.transition
   val ML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
   val SML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
@@ -15,7 +15,7 @@
 structure ML_File: ML_FILE =
 struct
 
-fun command environment debug get_file = Toplevel.generic_theory (fn gthy =>
+fun command environment catch_all debug get_file = Toplevel.generic_theory (fn gthy =>
   let
     val file = get_file (Context.theory_of gthy);
     val provide = Resources.provide_file file;
@@ -24,7 +24,7 @@
     val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
 
     val flags: ML_Compiler.flags =
-      {environment = environment, redirect = true, verbose = true,
+      {environment = environment, redirect = true, verbose = true, catch_all = catch_all,
         debug = debug, writeln = writeln, warning = warning};
   in
     gthy
@@ -34,7 +34,7 @@
     |> Context.mapping provide (Local_Theory.background_theory provide)
   end);
 
-val ML = command "";
-val SML = command ML_Env.SML;
+val ML = command "" false;
+val SML = command ML_Env.SML true;
 
 end;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML/ml_lex.ML	Fri Sep 29 11:19: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;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ML_Bootstrap.thy
--- a/src/Pure/ML_Bootstrap.thy	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ML_Bootstrap.thy	Fri Sep 29 11:19:43 2023 +0200
@@ -35,6 +35,6 @@
 
 setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
 
-declare [[ML_read_global = false]]
+declare [[ML_read_global = false, ML_catch_all = true]]
 
 end
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -81,7 +81,7 @@
                   let val _ = Position.report pos (Markup.language_path delimited) in
                     case content of
                       NONE =>
-                        Exn.interruptible_capture (fn () =>
+                        Exn.result (fn () =>
                           Resources.read_file_node file_node master_dir (src_path, pos)) ()
                     | SOME (digest, lines) => Exn.Res (blob_file src_path lines digest file_node)
                   end
@@ -193,11 +193,13 @@
     in Toplevel.command_errors int tr2 st end
   else Toplevel.command_errors int tr st;
 
+fun check_comments ctxt =
+  Document_Output.check_comments ctxt o Input.source_explode o Token.input_of;
+
 fun check_token_comments ctxt tok =
-  (Document_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); [])
-    handle exn =>
-      if Exn.is_interrupt exn then Exn.reraise exn
-      else Runtime.exn_messages exn;
+  (case Exn.result (fn () => check_comments ctxt tok) () of
+    Exn.Res () => []
+  | Exn.Exn exn => Runtime.exn_messages exn);
 
 fun check_span_comments ctxt span tr =
   Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) ();
@@ -222,7 +224,7 @@
 
 fun eval_state keywords span tr ({state, ...}: eval_state) =
   let
-    val _ = Thread_Attributes.expose_interrupt ();
+    val _ = Isabelle_Thread.expose_interrupt ();
 
     val st = reset_state keywords tr state;
 
@@ -298,11 +300,13 @@
 val print_functions =
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
+fun print_wrapper tr opt_context =
+  Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context;
+
 fun print_error tr opt_context e =
-  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
-    handle exn =>
-      if Exn.is_interrupt exn then Exn.reraise exn
-      else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn);
+  (case Exn.result (fn () => print_wrapper tr opt_context e ()) () of
+    Exn.Res res => res
+  | Exn.Exn exn => List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn));
 
 fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -550,6 +550,18 @@
           (fn deps => fn (name, node) =>
             if Symset.member required name orelse visible_node node orelse pending_result node then
               let
+                fun body () =
+                 (Execution.worker_task_active true name;
+                  if forall finished_import deps then
+                    iterate_entries (fn (_, opt_exec) => fn () =>
+                      (case opt_exec of
+                        SOME exec =>
+                          if Execution.is_running execution_id
+                          then SOME (Command.exec execution_id exec)
+                          else NONE
+                      | NONE => NONE)) node ()
+                  else ();
+                  Execution.worker_task_active false name);
                 val future =
                   (singleton o Future.forks)
                    {name = "theory:" ^ name,
@@ -557,21 +569,12 @@
                     deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
                     pri = 0, interrupts = false}
                   (fn () =>
-                   (Execution.worker_task_active true name;
-                    if forall finished_import deps then
-                      iterate_entries (fn (_, opt_exec) => fn () =>
-                        (case opt_exec of
-                          SOME exec =>
-                            if Execution.is_running execution_id
-                            then SOME (Command.exec execution_id exec)
-                            else NONE
-                        | NONE => NONE)) node ()
-                    else ();
-                    Execution.worker_task_active false name)
-                      handle exn =>
+                    (case Exn.capture body () of
+                      Exn.Res () => ()
+                    | Exn.Exn exn =>
                        (Output.system_message (Runtime.exn_message exn);
                         Execution.worker_task_active false name;
-                        Exn.reraise exn));
+                        Exn.reraise exn)));
               in (node, SOME (Future.task_of future)) end
             else (node, NONE));
       val execution' =
@@ -783,10 +786,10 @@
               Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
                 let
                   val _ = Output.status [Markup.markup_only Markup.consolidating];
-                  val res = Exn.capture (Thy_Info.apply_presentation context) thy;
+                  val result = Exn.capture (Thy_Info.apply_presentation context) thy;
                   val _ = Lazy.force (get_consolidated node);
                   val _ = Output.status [Markup.markup_only Markup.consolidated];
-                in Exn.release res end};
+                in Exn.release result end};
             val result_entry =
               (case lookup_entry node id of
                 NONE => err_undef "result command entry" id
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/protocol.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -164,8 +164,9 @@
 val _ =
   Protocol_Command.define "Document.dialog_result"
     (fn [serial, result] =>
-      Active.dialog_result (Value.parse_int serial) result
-        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
+      (case Exn.capture (fn () => Active.dialog_result (Value.parse_int serial) result) () of
+        Exn.Res () => ()
+      | Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn));
 
 val _ =
   Protocol_Command.define "ML_Heap.full_gc"
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/PIDE/protocol_command.ML
--- a/src/Pure/PIDE/protocol_command.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/protocol_command.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -40,8 +40,9 @@
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
-      (Runtime.exn_trace_system (fn () => cmd args)
-        handle exn =>
+      (case Exn.capture (fn () => Runtime.exn_trace_system (fn () => cmd args)) () of
+        Exn.Res res => res
+      | Exn.Exn exn =>
           if is_protocol_exn exn then Exn.reraise exn
           else error ("Isabelle protocol command failure: " ^ quote name)));
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/PIDE/query_operation.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -19,7 +19,7 @@
   Command.print_function (name ^ "_query")
     (fn {args = instance :: args, ...} =>
       SOME {delay = NONE, pri = pri, persistent = false, strict = false,
-        print_fn = fn _ => Thread_Attributes.uninterruptible (fn restore_attributes => fn state =>
+        print_fn = fn _ => Thread_Attributes.uninterruptible (fn run => fn state =>
           let
             fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
             fun status m = output_result (Markup.markup_only m);
@@ -28,11 +28,11 @@
               output_result (Markup.markup Markup.error (Runtime.exn_message exn));
 
             val _ = status Markup.running;
-            fun run () =
+            fun main () =
               f {state = state, args = args, output_result = output_result,
                   writeln_result = writeln_result};
             val _ =
-              (case Exn.capture (*sic!*) (restore_attributes run) () of
+              (case Exn.capture (*sic!*) (run main) () of
                 Exn.Res () => ()
               | Exn.Exn exn => toplevel_error exn);
             val _ = status Markup.finished;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Pure.thy	Fri Sep 29 11:19:43 2023 +0200
@@ -246,7 +246,7 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {environment = ML_Env.SML_export, redirect = false, verbose = true,
+          {environment = ML_Env.SML_export, redirect = false, verbose = true, catch_all = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
@@ -258,7 +258,7 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {environment = ML_Env.SML_import, redirect = false, verbose = true,
+          {environment = ML_Env.SML_import, redirect = false, verbose = true, catch_all = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
@@ -1558,4 +1558,6 @@
 
 declare [[ML_write_global = false]]
 
+ML_command \<open>\<^assert> (not (can ML_command \<open>() handle _ => ()\<close>))\<close>
+
 end
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/ROOT.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -28,6 +28,8 @@
 ML_file "Concurrent/unsynchronized.ML";
 ML_file "Concurrent/synchronized.ML";
 ML_file "Concurrent/counter.ML";
+ML_file "Concurrent/single_assignment.ML";
+ML_file "Concurrent/isabelle_thread.ML";
 
 ML_file "ML/ml_heap.ML";
 ML_file "ML/ml_print_depth0.ML";
@@ -121,8 +123,6 @@
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
-ML_file "Concurrent/single_assignment.ML";
-ML_file "Concurrent/isabelle_thread.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -215,7 +215,7 @@
         [ast] => ast
       | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
 
-    val ast = Exn.interruptible_capture ast_of parsetree;
+    val ast = Exn.result ast_of parsetree;
   in (! reports, ast) end;
 
 
@@ -310,7 +310,7 @@
                 SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t)
               | NONE => t);
 
-        val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
+        val tm' = Exn.result (fn () => decode [] [] [] tm) ();
       in (! reports, tm') end;
 
 end;
@@ -370,7 +370,7 @@
     val (ambig_msgs, asts) = parse_asts ctxt false root input;
     val results =
       (map o apsnd o Exn.maps_res)
-        (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
+        (Ast.normalize ctxt parse_rules #> Exn.result (ast_to_term ctxt tr)) asts;
   in (ambig_msgs, results) end;
 
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/command_line.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -13,11 +13,16 @@
 struct
 
 fun tool body =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
+      fun print_failure exn = (Runtime.exn_error_message exn; Exn.failure_rc exn);
       val rc =
-        (restore_attributes body (); 0) handle exn =>
-          ((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
-    in exit rc end) ();
+        (case Exn.capture (run body) () of
+          Exn.Res () => 0
+        | Exn.Exn exn =>
+            (case Exn.capture print_failure exn of
+              Exn.Res rc => rc
+            | Exn.Exn crash => Exn.failure_rc crash));
+    in exit rc end);
 
 end;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/isabelle_process.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -154,14 +154,20 @@
 
     fun protocol_loop () =
       let
-        val _ =
+        fun body () =
           (case Byte_Message.read_message in_stream of
             NONE => raise Protocol_Command.STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
-          | SOME (name :: args) => Protocol_Command.run (Bytes.content name) args)
-          handle exn =>
-            if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
-            else (Runtime.exn_system_message exn handle crash => recover crash);
+          | SOME (name :: args) => Protocol_Command.run (Bytes.content name) args);
+        val _ =
+          (case Exn.capture body () of
+            Exn.Res () => ()
+          | Exn.Exn exn =>
+              if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
+              else
+                (case Exn.capture Runtime.exn_system_message exn of
+                  Exn.Res () => ()
+                | Exn.Exn crash => recover crash));
       in protocol_loop () end;
 
     fun protocol () =
@@ -197,6 +203,7 @@
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
+  Isabelle_Thread.threads_stack_limit := Options.default_real "threads_stack_limit";
   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/isabelle_system.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -40,7 +40,7 @@
   let
     val {script, input, cwd, putenv, redirect, timeout, description} =
       Bash.dest_params params;
-    val run =
+    val server_run =
       [Bash.server_run, script, input,
         let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
         let open XML.Encode in YXML.string_of_body o list (pair string string) end
@@ -59,11 +59,11 @@
           with_streams (fn s => Byte_Message.write_message_string (#2 s) [Bash.server_kill, uuid])
       | kill NONE = ();
   in
-    Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+    Thread_Attributes.uninterruptible_body (fn run =>
       let
         fun err () = raise Fail "Malformed result from bash_process server";
-        fun loop maybe_uuid s =
-          (case restore_attributes Byte_Message.read_message_string (#1 s) of
+        fun loop_body s =
+          (case run Byte_Message.read_message_string (#1 s) of
             SOME (head :: args) =>
               if head = Bash.server_uuid andalso length args = 1 then
                 loop (SOME (hd args)) s
@@ -88,8 +88,13 @@
                  end
                else err ()
           | _ => err ())
-          handle exn => (kill maybe_uuid; Exn.reraise exn);
-      in with_streams (fn s => (Byte_Message.write_message_string (#2 s) run; loop NONE s)) end) ()
+        and loop maybe_uuid s =
+          (case Exn.capture (fn () => loop_body s) () of
+            Exn.Res res => res
+          | Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn));
+      in
+        with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s))
+      end)
   end;
 
 val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc;
@@ -138,18 +143,25 @@
       raise Fail ("Temporary file already exists: " ^ Path.print path);
   in path end;
 
-fun with_tmp_file name ext f =
-  let val path = create_tmp_path name ext
-  in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
+fun with_tmp_file name ext = Thread_Attributes.uninterruptible (fn run => fn f =>
+  let
+    val path = create_tmp_path name ext;
+    val result = Exn.capture (run f) path;
+    val _ = try File.rm path;
+  in Exn.release result end);
 
 
 (* tmp dirs *)
 
 fun rm_tree path = scala_function "rm_tree" [path];
 
-fun with_tmp_dir name f =
-  let val path = create_tmp_path name ""
-  in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
+fun with_tmp_dir name = Thread_Attributes.uninterruptible (fn run => fn f =>
+  let
+    val path = create_tmp_path name "";
+    val _ = make_directory path;
+    val result = Exn.capture (run f) path;
+    val _ = try rm_tree path;
+  in Exn.release result end);
 
 
 (* download file *)
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/System/scala.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -42,7 +42,7 @@
 in
 
 fun function_bytes name args =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       val id = new_id ();
       fun invoke () =
@@ -60,9 +60,10 @@
             | NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
     in
       invoke ();
-      Exn.release (restore_attributes await_result ())
-        handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
-    end) ();
+      (case Exn.capture (fn () => Exn.release (run await_result ())) () of
+        Exn.Res res => res
+      | Exn.Exn exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn))
+    end);
 
 val function1_bytes = singleton o function_bytes;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -216,9 +216,9 @@
   | consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
       let
         val _ = Execution.join [exec_id];
-        val res = Exn.capture Thm.consolidate_theory theory;
+        val result = Exn.capture Thm.consolidate_theory theory;
         val exns = maps Task_Queue.group_status (Execution.peek exec_id);
-      in res :: map Exn.Exn exns end;
+      in result :: map Exn.Exn exns end;
 
 fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
   | present_theory (Exn.Res (Result {theory, present, ...})) =
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/build.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -109,8 +109,12 @@
             else e ();
         in
           exec (fn () =>
-            (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn =>
-              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
+            (case Exn.capture (Future.interruptible_task build) () of
+              Exn.Res () => (0, [])
+            | Exn.Exn exn =>
+                (case Exn.capture Runtime.exn_message_list exn of
+                  Exn.Res errs => (1, errs)
+                | Exn.Exn _ (*sic!*) => (2, ["CRASHED"])))
           |> let open XML.Encode in pair int (list string) end
           |> single
           |> Output.protocol_message Markup.build_session_finished)
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/build.scala	Fri Sep 29 11:19:43 2023 +0200
@@ -856,7 +856,7 @@
 
     val errors = new mutable.ListBuffer[String]
     for (session_name <- sessions) {
-      Exn.interruptible_capture(print(session_name)) match {
+      Exn.result(print(session_name)) match {
         case Exn.Res(_) =>
         case Exn.Exn(exn) => errors += Exn.message(exn)
       }
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/debugger.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -29,10 +29,10 @@
 val warning_message = output_message Markup.warningN;
 val error_message = output_message Markup.errorN;
 
-fun error_wrapper e = e ()
-  handle exn =>
-    if Exn.is_interrupt exn then Exn.reraise exn
-    else error_message (Runtime.exn_message exn);
+fun error_wrapper e =
+  (case Exn.result e () of
+    Exn.Res res => res
+  | Exn.Exn exn => error_message (Runtime.exn_message exn));
 
 
 (* thread input *)
@@ -137,7 +137,7 @@
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {environment = environment SML, redirect = false, verbose = verbose,
+    {environment = environment SML, redirect = false, verbose = verbose, catch_all = SML,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;
 
@@ -229,13 +229,13 @@
 in
 
 fun debugger_loop thread_name =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       fun loop () =
         (debugger_state thread_name; if debugger_command thread_name then loop () else ());
-      val result = Exn.capture (restore_attributes with_debugging) loop;
+      val result = Exn.capture (run with_debugging) loop;
       val _ = debugger_state thread_name;
-    in Exn.release result end) ();
+    in Exn.release result end);
 
 end;
 
diff -r 4de5b127c124 -r a9ac75d397df src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -400,17 +400,24 @@
 
 val _ =
   Protocol_Command.define "Simplifier_Trace.reply"
-    (fn [serial_string, reply] =>
-      let
-        val serial = Value.parse_int serial_string
-        val result =
-          Synchronized.change_result futures
-            (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
-      in
-        (case result of
-          SOME promise => Future.fulfill promise reply
-        | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
-      end handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
+    let
+      fun body serial_string reply =
+        let
+          val serial = Value.parse_int serial_string
+          val result =
+            Synchronized.change_result futures
+              (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
+        in
+          (case result of
+            SOME promise => Future.fulfill promise reply
+          | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
+        end
+    in
+      fn [serial_string, reply] =>
+        (case Exn.capture (fn () => body serial_string reply) () of
+          Exn.Res () => ()
+        | Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
+    end;
 
 
 
diff -r 4de5b127c124 -r a9ac75d397df src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -99,7 +99,7 @@
     val (program_code, value_name) = comp vs_t;
     val value_code = space_implode " "
       (value_name :: "()" :: map (enclose "(" ")") args);
-  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
+  in Exn.result (value ctxt cookie) (program_code, value_code) end;
 
 fun partiality_as_none e = SOME (Exn.release e)
   handle General.Match => NONE
@@ -390,7 +390,7 @@
 
 fun checked_computation cTs raw_computation ctxt =
   check_computation_input ctxt cTs
-  #> Exn.interruptible_capture raw_computation
+  #> Exn.result raw_computation
   #> partiality_as_none;
 
 fun mount_computation ctxt cTs T raw_computation lift_postproc =
diff -r 4de5b127c124 -r a9ac75d397df src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Tools/quickcheck.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -262,7 +262,7 @@
       try tester v
     else
       let (* FIXME !?!? *)
-        val tester = Exn.interruptible_capture tester v
+        val tester = Exn.result tester v
       in
         (case Exn.get_res tester of
           NONE => SOME (Exn.release tester)
diff -r 4de5b127c124 -r a9ac75d397df src/Tools/try.ML
--- a/src/Tools/try.ML	Wed Sep 27 13:34:15 2023 +0100
+++ b/src/Tools/try.ML	Fri Sep 29 11:19:43 2023 +0200
@@ -83,17 +83,18 @@
           persistent = true,
           strict = true,
           print_fn = fn _ => fn st =>
-            let
-              val state = Toplevel.proof_of st
-                |> Proof.map_context (Context_Position.set_visible false)
-              val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
-            in
-              if auto_time_limit > 0.0 then
-                (case Timeout.apply_physical (seconds auto_time_limit) (fn () => body true state) () of
-                  (true, (_, outcome)) => List.app Output.information outcome
-                | _ => ())
-              else ()
-            end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
+            \<^try>\<open>
+              let
+                val state = Toplevel.proof_of st
+                  |> Proof.map_context (Context_Position.set_visible false)
+                val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
+              in
+                if auto_time_limit > 0.0 then
+                  (case Timeout.apply_physical (seconds auto_time_limit) (fn () => body true state) () of
+                    (true, (_, outcome)) => List.app Output.information outcome
+                  | _ => ())
+                else ()
+              end catch _ => ()\<close>}
       else NONE);