src/Pure/ML-Systems/multithreading.ML
changeset 28160 e0177b67ecd9
parent 28149 26bd1245a46b
child 28169 356fc8734741
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Sun Sep 07 22:20:08 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Sun Sep 07 22:20:11 2008 +0200
     1.3 @@ -20,6 +20,10 @@
     1.4    val max_threads: int ref
     1.5    val max_threads_value: unit -> int
     1.6    val no_interrupts: Thread.threadAttribute list
     1.7 +  val sync_interrupts: Thread.threadAttribute list
     1.8 +  val regular_interrupts: Thread.threadAttribute list
     1.9 +  val with_attributes: Thread.threadAttribute list ->
    1.10 +    (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    1.11    val self_critical: unit -> bool
    1.12    val serial: unit -> int
    1.13  end;
    1.14 @@ -37,6 +41,10 @@
    1.15  fun max_threads_value () = Int.max (! max_threads, 1);
    1.16  
    1.17  val no_interrupts = [];
    1.18 +val sync_interrupts = [];
    1.19 +val regular_interrupts = [];
    1.20 +
    1.21 +fun with_attributes _ f x = f [] x;
    1.22  
    1.23  
    1.24  (* critical section *)
    1.25 @@ -55,4 +63,3 @@
    1.26  
    1.27  structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    1.28  open BasicMultithreading;
    1.29 -