src/Pure/ML-Systems/multithreading_polyml.ML
changeset 24144 ec51a0f7eefe
parent 24119 06965b38c5e9
child 24208 f4cafbaa05e4
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Aug 03 16:28:22 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Aug 03 16:28:23 2007 +0200
     1.3 @@ -53,17 +53,17 @@
     1.4    if self_critical () then e ()
     1.5    else
     1.6      let
     1.7 +      val name' = ! critical_name;
     1.8        val _ =
     1.9          if Mutex.trylock critical_lock then ()
    1.10          else
    1.11            let
    1.12              val timer = Timer.startRealTimer ();
    1.13 -            val _ = tracing 3 (fn () =>
    1.14 -              "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": waiting");
    1.15 +            val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    1.16              val _ = Mutex.lock critical_lock;
    1.17 -            val _ = tracing 3 (fn () =>
    1.18 -              "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": passed after " ^
    1.19 -              Time.toString (Timer.checkRealTimer timer));
    1.20 +            val time = Timer.checkRealTimer timer;
    1.21 +            val _ = tracing (if Time.> (time, Time.fromMilliseconds 10) then 3 else 4) (fn () =>
    1.22 +              "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    1.23            in () end;
    1.24        val _ = critical_thread := SOME (Thread.self ());
    1.25        val _ = critical_name := name;
    1.26 @@ -92,12 +92,15 @@
    1.27      val lock = Mutex.mutex ();
    1.28      fun PROTECTED name e =
    1.29        let
    1.30 +        val name' = ! protected_name;
    1.31          val _ =
    1.32            if Mutex.trylock lock then ()
    1.33            else
    1.34 -           (tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting");
    1.35 -            Mutex.lock lock;
    1.36 -            tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed"));
    1.37 +            let
    1.38 +              val _ = tracing 2 (fn () => "PROTECTED" ^ show name ^ show' name' ^ ": waiting");
    1.39 +              val _ = Mutex.lock lock;
    1.40 +              val _ = tracing 2 (fn () => "PROTECTED" ^ show name ^ show' name' ^ ": passed");
    1.41 +            in () end;
    1.42          val _ = protected_name := name;
    1.43          val res = Exn.capture e ();
    1.44          val _ = protected_name := "";