--- a/src/Pure/ML-Systems/multithreading.ML Fri Mar 20 20:05:51 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML Fri Mar 20 20:20:09 2009 +0100
@@ -21,6 +21,7 @@
val enabled: unit -> bool
val no_interrupts: Thread.threadAttribute list
val regular_interrupts: Thread.threadAttribute list
+ val restricted_interrupts: Thread.threadAttribute list
val with_attributes: Thread.threadAttribute list ->
(Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
val self_critical: unit -> bool
@@ -46,6 +47,9 @@
val regular_interrupts =
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
+val restricted_interrupts =
+ [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+
fun with_attributes _ f x = f [] x;