# HG changeset patch
# User wenzelm
# Date 1460203891 -7200
# Node ID ce47945ce4fb104109a748f3634a4ee7e8e8d7e7
# Parent  3a122e1e352a1100edf0889a133ceb0368106e3a
tuned signature -- closer to Exn.Interrupt.expose in Scala;

diff -r 3a122e1e352a -r ce47945ce4fb src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Apr 09 14:00:23 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Apr 09 14:11:31 2016 +0200
@@ -211,7 +211,7 @@
      then Thread_Attributes.private_interrupts
      else Thread_Attributes.public_interrupts)
     (fn _ => f x)
-  before Multithreading.interrupted ();
+  before Thread_Attributes.expose_interrupt ();
 
 
 (* worker threads *)
@@ -231,7 +231,7 @@
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
-        val test = Exn.capture Multithreading.interrupted ();
+        val test = Exn.capture Thread_Attributes.expose_interrupt ();
         val _ =
           if ok andalso not (Exn.is_interrupt_exn test) then ()
           else if null (cancel_now group) then ()
diff -r 3a122e1e352a -r ce47945ce4fb src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:00:23 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:11:31 2016 +0200
@@ -6,7 +6,6 @@
 
 signature MULTITHREADING =
 sig
-  val interrupted: unit -> unit  (*exception Interrupt*)
   val max_threads_value: unit -> int
   val max_threads_update: int -> unit
   val enabled: unit -> bool
@@ -22,17 +21,6 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* interrupts *)
-
-fun interrupted () =
-  let
-    val orig_atts = Thread_Attributes.safe_interrupts (Thread.getAttributes ());
-    val _ = Thread.setAttributes Thread_Attributes.test_interrupts;
-    val test = Exn.capture Thread.testInterrupt ();
-    val _ = Thread.setAttributes orig_atts;
-  in Exn.release test end;
-
-
 (* options *)
 
 fun num_processors () =
diff -r 3a122e1e352a -r ce47945ce4fb src/Pure/Concurrent/thread_attributes.ML
--- a/src/Pure/Concurrent/thread_attributes.ML	Sat Apr 09 14:00:23 2016 +0200
+++ b/src/Pure/Concurrent/thread_attributes.ML	Sat Apr 09 14:11:31 2016 +0200
@@ -15,6 +15,7 @@
   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 =
@@ -60,4 +61,12 @@
   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 (Thread.Thread.getAttributes ());
+    val _ = Thread.Thread.setAttributes test_interrupts;
+    val test = Exn.capture Thread.Thread.testInterrupt ();
+    val _ = Thread.Thread.setAttributes orig_atts;
+  in Exn.release test end;
+
 end;
diff -r 3a122e1e352a -r ce47945ce4fb src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Sat Apr 09 14:00:23 2016 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Sat Apr 09 14:11:31 2016 +0200
@@ -30,7 +30,7 @@
 
       val stop = Time.now ();
       val was_timeout = not (Event_Timer.cancel request);
-      val test = Exn.capture Multithreading.interrupted ();
+      val test = Exn.capture Thread_Attributes.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 3a122e1e352a -r ce47945ce4fb src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Apr 09 14:00:23 2016 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Apr 09 14:11:31 2016 +0200
@@ -216,7 +216,7 @@
 
 fun eval_state keywords span tr ({state, ...}: eval_state) =
   let
-    val _ = Multithreading.interrupted ();
+    val _ = Thread_Attributes.expose_interrupt ();
 
     val st = reset_state keywords tr state;