diff -r 591fefcf184e -r cb6421b6a18f src/Pure/ML-Systems/multithreading.ML --- 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;