src/Pure/ML-Systems/multithreading.ML
changeset 32185 57ecfab3bcfe
parent 32184 cfa0ef0c0c5f
child 32186 8026b73cd357
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:13:39 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:39:05 2009 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    val trace: int ref
     1.5    val tracing: int -> (unit -> string) -> unit
     1.6    val tracing_time: Time.time -> (unit -> string) -> unit
     1.7 +  val real_time: ('a -> unit) -> 'a -> Time.time
     1.8    val available: bool
     1.9    val max_threads: int ref
    1.10    val max_threads_value: unit -> int
    1.11 @@ -32,11 +33,15 @@
    1.12  structure Multithreading: MULTITHREADING =
    1.13  struct
    1.14  
    1.15 -(* options *)
    1.16 +(* tracing *)
    1.17  
    1.18  val trace = ref (0: int);
    1.19  fun tracing _ _ = ();
    1.20  fun tracing_time _ _ = ();
    1.21 +fun real_time f x = (f x; Time.zeroTime);
    1.22 +
    1.23 +
    1.24 +(* options *)
    1.25  
    1.26  val available = false;
    1.27  val max_threads = ref (1: int);