src/Pure/ML-Systems/multithreading.ML
changeset 32286 1fb5db48002d
parent 32186 8026b73cd357
child 32295 400cc493d466
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Thu Jul 30 18:43:52 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Thu Jul 30 23:06:06 2009 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val restricted_interrupts: Thread.threadAttribute list
     1.5    val with_attributes: Thread.threadAttribute list ->
     1.6      (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
     1.7 +  val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool
     1.8    val self_critical: unit -> bool
     1.9    val serial: unit -> int
    1.10  end;
    1.11 @@ -48,6 +49,9 @@
    1.12  fun max_threads_value () = 1: int;
    1.13  fun enabled () = false;
    1.14  
    1.15 +
    1.16 +(* attributes *)
    1.17 +
    1.18  val no_interrupts =
    1.19    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    1.20  
    1.21 @@ -59,6 +63,8 @@
    1.22  
    1.23  fun with_attributes _ f x = f [] x;
    1.24  
    1.25 +fun sync_wait _ _ _ = false;
    1.26 +
    1.27  
    1.28  (* critical section *)
    1.29  
    1.30 @@ -74,5 +80,5 @@
    1.31  
    1.32  end;
    1.33  
    1.34 -structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    1.35 -open BasicMultithreading;
    1.36 +structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
    1.37 +open Basic_Multithreading;