# HG changeset patch
# User wenzelm
# Date 1297170564 -3600
# Node ID a21084741b376b4ef4289140f3943e9168086660
# Parent  82339c3fd74ac9bcf47d1e395ac32f3d2825373b
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);

diff -r 82339c3fd74a -r a21084741b37 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Mon Feb 07 23:57:03 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Tue Feb 08 14:09:24 2011 +0100
@@ -21,6 +21,7 @@
   val public_interrupts: Thread.threadAttribute list
   val private_interrupts: Thread.threadAttribute list
   val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
+  val interrupted: unit -> unit  (*exception Interrupt*)
   val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
     ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
@@ -50,6 +51,8 @@
 val private_interrupts = [];
 fun sync_interrupts _ = [];
 
+fun interrupted () = ();
+
 fun with_attributes _ e = e [];
 
 fun sync_wait _ _ _ _ = Exn.Result true;
diff -r 82339c3fd74a -r a21084741b37 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Feb 07 23:57:03 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 08 14:09:24 2011 +0100
@@ -45,6 +45,9 @@
 val no_interrupts =
   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
 
+val test_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
+
 val public_interrupts =
   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
 
@@ -61,6 +64,14 @@
       Thread.InterruptState Thread.InterruptAsynchOnce
     | x => x);
 
+fun interrupted () =
+  let
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
+    val _ = Thread.setAttributes test_interrupts;
+    val test = Exn.capture Thread.testInterrupt ();
+    val _ = Thread.setAttributes orig_atts;
+  in Exn.release test end;
+
 fun with_attributes new_atts e =
   let
     val orig_atts = safe_interrupts (Thread.getAttributes ());