--- 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 ());