# HG changeset patch
# User wenzelm
# Date 1695671938 -7200
# Node ID eb2255d241da2091b5d3aab024469ad89326fc02
# Parent  a44ac17ae227100ac544083d62033901ef988d3a
clarified signature;

diff -r a44ac17ae227 -r eb2255d241da src/Pure/Concurrent/future.ML
--- 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 ()
diff -r a44ac17ae227 -r eb2255d241da src/Pure/Concurrent/isabelle_thread.ML
--- 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 () =>
diff -r a44ac17ae227 -r eb2255d241da src/Pure/Concurrent/timeout.ML
--- 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)