# HG changeset patch
# User wenzelm
# Date 1697018364 -7200
# Node ID 461e924cc82526701c37c45be58c17680c9c6609
# Parent  05da36bc806f6b8dffa3b71e444172a55ca71b0f
proper Exn.capture / Isabelle_Thread.try_catch;

diff -r 05da36bc806f -r 461e924cc825 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Oct 11 11:37:18 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Oct 11 11:59:24 2023 +0200
@@ -279,7 +279,7 @@
 fun scheduler_end () = (*requires SYNCHRONIZED*)
   (ML_statistics (); scheduler := NONE);
 
-fun scheduler_next () = (*requires SYNCHRONIZED*)
+fun scheduler_next0 () = (*requires SYNCHRONIZED*)
   let
     val now = Time.now ();
     val tick = ! last_round + next_round <= now;
@@ -354,15 +354,19 @@
     val _ = if continue then () else scheduler_end ();
 
     val _ = broadcast scheduler_event;
-  in continue end
-  handle exn =>
-   (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
-    if Exn.is_interrupt exn then
-     (List.app cancel_later (cancel_all ());
-      signal work_available; true)
-    else
-     (scheduler_end ();
-      Exn.reraise exn));
+  in continue end;
+
+fun scheduler_next () =
+  (case Exn.capture_body scheduler_next0 of
+    Exn.Res res => res
+  | Exn.Exn exn =>
+     (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
+      if Exn.is_interrupt exn then
+       (List.app cancel_later (cancel_all ());
+        signal work_available; true)
+      else
+       (scheduler_end ();
+        Exn.reraise exn)));
 
 fun scheduler_loop () =
  (while
@@ -417,11 +421,13 @@
 
 fun assign_result group result res =
   let
-    val _ = Single_Assignment.assign result res
-      handle exn as Fail _ =>
-        (case Single_Assignment.peek result of
-          SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
-        | _ => Exn.reraise exn);
+    val _ =
+      (case Exn.capture_body (fn () => Single_Assignment.assign result res) of
+        Exn.Exn (exn as Fail _) =>
+          (case Single_Assignment.peek result of
+            SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
+          | _ => Exn.reraise exn)
+      | _ => ());
     val ok =
       (case the (Single_Assignment.peek result) of
         Exn.Exn exn =>
@@ -554,8 +560,9 @@
       val futures =
         forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
     in
-      run join_results futures
-        handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
+      (case Exn.capture_body (fn () => run join_results futures) of
+        Exn.Res res => res
+      | Exn.Exn exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn))
     end);
 
 
@@ -639,12 +646,14 @@
   let
     val group = worker_subgroup ();
     val result = Single_Assignment.var "promise" : 'a result;
-    fun assign () = assign_result group result Isabelle_Thread.interrupt_exn
-      handle Fail _ => true
-        | exn =>
-            if Exn.is_interrupt exn
-            then raise Fail "Concurrent attempt to fulfill promise"
-            else Exn.reraise exn;
+    fun assign () =
+      (case Exn.capture_body (fn () => assign_result group result Isabelle_Thread.interrupt_exn) of
+        Exn.Res res => res
+      | Exn.Exn (Fail _) => true
+      | Exn.Exn exn =>
+          if Exn.is_interrupt exn
+          then raise Fail "Concurrent attempt to fulfill promise"
+          else Exn.reraise exn);
     fun job () =
       Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
         (fn _ => Exn.release (Exn.capture assign () before abort ()));
diff -r 05da36bc806f -r 461e924cc825 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Oct 11 11:37:18 2023 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Oct 11 11:59:24 2023 +0200
@@ -197,17 +197,16 @@
   (f |> debugging opt_context |> Future.interruptible_task
     |> ML_Profiling.profile (Options.default_string "profiling")) x;
 
-fun toplevel_error output_exn f x = f x
-  handle exn =>
-    if Exn.is_interrupt exn then Exn.reraise exn
-    else
+fun toplevel_error output_exn f x =
+  Isabelle_Thread.try_catch (fn () => f x)
+    (fn exn =>
       let
         val opt_ctxt =
           (case Context.get_generic_context () of
             NONE => NONE
           | SOME context => try Context.proof_of context);
         val _ = output_exn (exn_context opt_ctxt exn);
-      in raise TOPLEVEL_ERROR end;
+      in raise TOPLEVEL_ERROR end);
 
 fun toplevel_program body =
   (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
diff -r 05da36bc806f -r 461e924cc825 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Oct 11 11:37:18 2023 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Oct 11 11:59:24 2023 +0200
@@ -299,11 +299,11 @@
       PolyML.Compiler.CPBindingSeq serial];
 
     val _ =
-      (while not (List.null (! input_buffer)) do
-        ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ()))
-      handle exn =>
-        if Exn.is_interrupt exn then Exn.reraise exn
-        else
+      Isabelle_Thread.try_catch
+        (fn () =>
+          (while not (List.null (! input_buffer)) do
+            ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ())))
+        (fn exn =>
           let
             val exn_msg =
               (case exn of
@@ -311,7 +311,7 @@
               | Runtime.TOPLEVEL_ERROR => ""
               | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
             val _ = err exn_msg;
-          in expose_error true end;
+          in expose_error true end);
   in expose_error (#verbose flags) end;
 
 end;
diff -r 05da36bc806f -r 461e924cc825 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Wed Oct 11 11:37:18 2023 +0200
+++ b/src/Pure/morphism.ML	Wed Oct 11 11:59:24 2023 +0200
@@ -83,9 +83,9 @@
 
 exception MORPHISM of string * exn;
 
-fun app context (name, f) x = f context x
-  handle exn =>
-    if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
+fun app context (name, f) x =
+  Isabelle_Thread.try_catch (fn () => f context x)
+    (fn exn => raise MORPHISM (name, exn));
 
 
 (* optional context *)
diff -r 05da36bc806f -r 461e924cc825 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Oct 11 11:37:18 2023 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 11 11:59:24 2023 +0200
@@ -2238,14 +2238,17 @@
 
     val open_proof = not named ? rew_proof thy;
 
+    fun export_body () = join_proof body' |> open_proof |> export_proof thy i prop1;
     val export =
       if export_enabled () then
         Lazy.lazy (fn () =>
-          join_proof body' |> open_proof |> export_proof thy i prop1 handle exn =>
-            if Exn.is_interrupt exn then
-              raise Fail ("Interrupt: potential resource problems while exporting proof " ^
-                string_of_int i)
-            else Exn.reraise exn)
+          (case Exn.capture_body export_body of
+            Exn.Res res => res
+          | Exn.Exn exn =>
+              if Exn.is_interrupt exn then
+                raise Fail ("Interrupt: potential resource problems while exporting proof " ^
+                  string_of_int i)
+              else Exn.reraise exn))
       else no_export;
 
     val thm_body = prune_body body';