# HG changeset patch
# User wenzelm
# Date 1695671198 -7200
# Node ID a44ac17ae227100ac544083d62033901ef988d3a
# Parent  c2c4d51b048bfd6f2c36586f5f4c264f2b22387c
clarified modules;

diff -r c2c4d51b048b -r a44ac17ae227 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Sep 25 21:36:46 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Sep 25 21:46:38 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 = Exn.capture Isabelle_Thread.expose_interrupt ();
         val _ =
           if ok andalso not (Exn.is_interrupt_exn test) then ()
           else if null (cancel_now group) then ()
diff -r c2c4d51b048b -r a44ac17ae227 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 21:36:46 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 21:46:38 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: 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
@@ -121,6 +122,14 @@
 fun interrupt_other t =
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
+fun expose_interrupt () =
+  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;
+
 fun try_catch e f =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     restore_attributes e ()
diff -r c2c4d51b048b -r a44ac17ae227 src/Pure/Concurrent/thread_attributes.ML
--- a/src/Pure/Concurrent/thread_attributes.ML	Mon Sep 25 21:36:46 2023 +0200
+++ b/src/Pure/Concurrent/thread_attributes.ML	Mon Sep 25 21:46:38 2023 +0200
@@ -18,7 +18,6 @@
   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*)
 end;
 
 structure Thread_Attributes: THREAD_ATTRIBUTES =
@@ -107,12 +106,4 @@
   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;
-
 end;
diff -r c2c4d51b048b -r a44ac17ae227 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Mon Sep 25 21:36:46 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Mon Sep 25 21:46:38 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 = Exn.capture Isabelle_Thread.expose_interrupt ();
       in
         if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
         then raise TIMEOUT (stop - start)
diff -r c2c4d51b048b -r a44ac17ae227 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Sep 25 21:36:46 2023 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Sep 25 21:46:38 2023 +0200
@@ -222,7 +222,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;