# HG changeset patch
# User wenzelm
# Date 1220996916 -7200
# Node ID 4062882c7df3b37884228953723d82711c8f718d
# Parent  6a8417f368371ce08a359b3315ada8a3cc685289
proper values of no_interrupts, regular_interrupts;

diff -r 6a8417f36837 -r 4062882c7df3 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Tue Sep 09 23:30:05 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Tue Sep 09 23:48:36 2008 +0200
@@ -39,8 +39,11 @@
 val max_threads = ref (1: int);
 fun max_threads_value () = Int.max (! max_threads, 1);
 
-val no_interrupts = [];
-val regular_interrupts = [];
+val no_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+
+val regular_interrupts =
+  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
 
 fun with_attributes _ f x = f [] x;