# HG changeset patch
# User wenzelm
# Date 1220818811 -7200
# Node ID e0177b67ecd9dbb97c13420306290c58631fd37f
# Parent  80823c582b9dc1b40788bb65ea39d1b32300742a
added sync_interrupts, regular_interrupts;

diff -r 80823c582b9d -r e0177b67ecd9 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;
-