src/Pure/ML-Systems/multithreading.ML

--- a/src/Pure/ML-Systems/multithreading.ML	Sun Sep 07 22:20:08 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Sun Sep 07 22:20:11 2008 +0200
@@ -20,6 +20,10 @@
   val max_threads: int ref
   val max_threads_value: unit -> int
   val no_interrupts: Thread.threadAttribute list
+  val sync_interrupts: Thread.threadAttribute list
+  val regular_interrupts: Thread.threadAttribute list
+  val with_attributes: Thread.threadAttribute list ->
+    (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
   val self_critical: unit -> bool
   val serial: unit -> int
 end;
@@ -37,6 +41,10 @@
 fun max_threads_value () = Int.max (! max_threads, 1);
 
 val no_interrupts = [];
+val sync_interrupts = [];
+val regular_interrupts = [];
+
+fun with_attributes _ f x = f [] x;
 
 
 (* critical section *)
@@ -55,4 +63,3 @@
 
 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
 open BasicMultithreading;
-