--- a/src/Pure/Concurrent/future.ML Mon Sep 25 21:46:38 2023 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Sep 25 21:58:58 2023 +0200
@@ -234,7 +234,7 @@
val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
- val test = Exn.capture Isabelle_Thread.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 ()
--- a/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 25 21:46:38 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 25 21:58:58 2023 +0200
@@ -25,6 +25,7 @@
val interrupt_exn: 'a Exn.result
val interrupt_self: unit -> 'a
val interrupt_other: T -> unit
+ 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
@@ -122,13 +123,15 @@
fun interrupt_other t =
Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
-fun expose_interrupt () =
+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 Exn.release test end;
+ in test end;
+
+val expose_interrupt = Exn.release o expose_interrupt_result;
fun try_catch e f =
Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
--- a/src/Pure/Concurrent/timeout.ML Mon Sep 25 21:46:38 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML Mon Sep 25 21:58:58 2023 +0200
@@ -46,7 +46,7 @@
val stop = Time.now ();
val was_timeout = not (Event_Timer.cancel request);
- val test = Exn.capture Isabelle_Thread.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)