src/Pure/ML-Systems/multithreading_polyml.ML
changeset 32738 15bb09ca0378
parent 32295 400cc493d466
child 33180 e1b0280f0299
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  val available = true;
     1.6  
     1.7 -val max_threads = ref 0;
     1.8 +val max_threads = Unsynchronized.ref 0;
     1.9  
    1.10  val tested_platform =
    1.11    let val ml_platform = getenv "ML_PLATFORM"
    1.12 @@ -114,7 +114,7 @@
    1.13  
    1.14  (* tracing *)
    1.15  
    1.16 -val trace = ref 0;
    1.17 +val trace = Unsynchronized.ref 0;
    1.18  
    1.19  fun tracing level msg =
    1.20    if level > ! trace then ()
    1.21 @@ -148,7 +148,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 = ref false;
    1.26 +    val timeout = Unsynchronized.ref false;
    1.27      val watchdog = Thread.fork (fn () =>
    1.28        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
    1.29  
    1.30 @@ -173,7 +173,7 @@
    1.31  
    1.32      (*result state*)
    1.33      datatype result = Wait | Signal | Result of int;
    1.34 -    val result = ref Wait;
    1.35 +    val result = Unsynchronized.ref Wait;
    1.36      val lock = Mutex.mutex ();
    1.37      val cond = ConditionVar.conditionVar ();
    1.38      fun set_result res =
    1.39 @@ -231,8 +231,8 @@
    1.40  local
    1.41  
    1.42  val critical_lock = Mutex.mutex ();
    1.43 -val critical_thread = ref (NONE: Thread.thread option);
    1.44 -val critical_name = ref "";
    1.45 +val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
    1.46 +val critical_name = Unsynchronized.ref "";
    1.47  
    1.48  in
    1.49  
    1.50 @@ -274,7 +274,7 @@
    1.51  local
    1.52  
    1.53  val serial_lock = Mutex.mutex ();
    1.54 -val serial_count = ref 0;
    1.55 +val serial_count = Unsynchronized.ref 0;
    1.56  
    1.57  in
    1.58