src/Pure/ML-Systems/multithreading.ML
changeset 32776 1504f9c2d060
parent 32295 400cc493d466
child 32777 8ae3a48c69d9
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Wed Sep 30 09:25:18 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Wed Sep 30 11:36:12 2009 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  sig
     1.5    include BASIC_MULTITHREADING
     1.6    val available: bool
     1.7 -  val max_threads: int ref
     1.8 +  val max_threads: int Unsynchronized.ref
     1.9    val max_threads_value: unit -> int
    1.10    val enabled: unit -> bool
    1.11    val no_interrupts: Thread.threadAttribute list
    1.12 @@ -24,7 +24,7 @@
    1.13    val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
    1.14    val sync_wait: Thread.threadAttribute list option -> Time.time option ->
    1.15      ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
    1.16 -  val trace: int ref
    1.17 +  val trace: int  Unsynchronized.ref
    1.18    val tracing: int -> (unit -> string) -> unit
    1.19    val tracing_time: bool -> Time.time -> (unit -> string) -> unit
    1.20    val real_time: ('a -> unit) -> 'a -> Time.time
    1.21 @@ -38,7 +38,7 @@
    1.22  (* options *)
    1.23  
    1.24  val available = false;
    1.25 -val max_threads = ref (1: int);
    1.26 +val max_threads =  Unsynchronized.ref (1: int);
    1.27  fun max_threads_value () = 1: int;
    1.28  fun enabled () = false;
    1.29  
    1.30 @@ -57,7 +57,7 @@
    1.31  
    1.32  (* tracing *)
    1.33  
    1.34 -val trace = ref (0: int);
    1.35 +val trace =  Unsynchronized.ref (0: int);
    1.36  fun tracing _ _ = ();
    1.37  fun tracing_time _ _ _ = ();
    1.38  fun real_time f x = (f x; Time.zeroTime);
    1.39 @@ -72,7 +72,7 @@
    1.40  
    1.41  (* serial numbers *)
    1.42  
    1.43 -local val count = ref (0: int)
    1.44 +local val count =  Unsynchronized.ref (0: int)
    1.45  in fun serial () = (count := ! count + 1; ! count) end;
    1.46  
    1.47  end;