src/Pure/ML-Systems/multithreading_polyml.ML
changeset 39616 8052101883c3
parent 39583 c1e9c6dfeff8
child 40301 bf39a257b3d3
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 17:46:59 2010 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 18:21:48 2010 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  val available = true;
     1.6  
     1.7 -val max_threads = Unsynchronized.ref 0;
     1.8 +val max_threads = ref 0;
     1.9  
    1.10  fun max_threads_value () =
    1.11    let val m = ! max_threads in
    1.12 @@ -109,7 +109,7 @@
    1.13  
    1.14  (* tracing *)
    1.15  
    1.16 -val trace = Unsynchronized.ref 0;
    1.17 +val trace = ref 0;
    1.18  
    1.19  fun tracing level msg =
    1.20    if level > ! trace then ()
    1.21 @@ -143,7 +143,7 @@
    1.22  fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
    1.23    let
    1.24      val worker = Thread.self ();
    1.25 -    val timeout = Unsynchronized.ref false;
    1.26 +    val timeout = ref false;
    1.27      val watchdog = Thread.fork (fn () =>
    1.28        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
    1.29  
    1.30 @@ -168,7 +168,7 @@
    1.31  
    1.32      (*result state*)
    1.33      datatype result = Wait | Signal | Result of int;
    1.34 -    val result = Unsynchronized.ref Wait;
    1.35 +    val result = ref Wait;
    1.36      val lock = Mutex.mutex ();
    1.37      val cond = ConditionVar.conditionVar ();
    1.38      fun set_result res =
    1.39 @@ -226,8 +226,8 @@
    1.40  local
    1.41  
    1.42  val critical_lock = Mutex.mutex ();
    1.43 -val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
    1.44 -val critical_name = Unsynchronized.ref "";
    1.45 +val critical_thread = ref (NONE: Thread.thread option);
    1.46 +val critical_name = ref "";
    1.47  
    1.48  in
    1.49  
    1.50 @@ -269,7 +269,7 @@
    1.51  local
    1.52  
    1.53  val serial_lock = Mutex.mutex ();
    1.54 -val serial_count = Unsynchronized.ref 0;
    1.55 +val serial_count = ref 0;
    1.56  
    1.57  in
    1.58