--- 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 ()));
--- 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) ();
--- 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;
--- 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 *)
--- 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';