tuned whitespace;
authorwenzelm
Wed Sep 30 11:45:42 2009 +0200 (2009-09-30)
changeset 327778ae3a48c69d9
parent 32776 1504f9c2d060
child 32778 a92a18253f1e
child 32779 371c7f74282d
tuned whitespace;
src/Pure/ML-Systems/multithreading.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Wed Sep 30 11:36:12 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Wed Sep 30 11:45:42 2009 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
     1.5    val sync_wait: Thread.threadAttribute list option -> Time.time option ->
     1.6      ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
     1.7 -  val trace: int  Unsynchronized.ref
     1.8 +  val trace: int Unsynchronized.ref
     1.9    val tracing: int -> (unit -> string) -> unit
    1.10    val tracing_time: bool -> Time.time -> (unit -> string) -> unit
    1.11    val real_time: ('a -> unit) -> 'a -> Time.time
    1.12 @@ -38,7 +38,7 @@
    1.13  (* options *)
    1.14  
    1.15  val available = false;
    1.16 -val max_threads =  Unsynchronized.ref (1: int);
    1.17 +val max_threads = Unsynchronized.ref (1: int);
    1.18  fun max_threads_value () = 1: int;
    1.19  fun enabled () = false;
    1.20  
    1.21 @@ -57,7 +57,7 @@
    1.22  
    1.23  (* tracing *)
    1.24  
    1.25 -val trace =  Unsynchronized.ref (0: int);
    1.26 +val trace = Unsynchronized.ref (0: int);
    1.27  fun tracing _ _ = ();
    1.28  fun tracing_time _ _ _ = ();
    1.29  fun real_time f x = (f x; Time.zeroTime);
    1.30 @@ -72,7 +72,7 @@
    1.31  
    1.32  (* serial numbers *)
    1.33  
    1.34 -local val count =  Unsynchronized.ref (0: int)
    1.35 +local val count = Unsynchronized.ref (0: int)
    1.36  in fun serial () = (count := ! count + 1; ! count) end;
    1.37  
    1.38  end;