src/Pure/ML-Systems/multithreading_polyml.ML
changeset 24119 06965b38c5e9
parent 24109 952efb77cf91
child 24144 ec51a0f7eefe
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 01 16:59:15 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Aug 01 17:03:28 2007 +0200
     1.3 @@ -12,9 +12,9 @@
     1.4  
     1.5  (* options *)
     1.6  
     1.7 -val trace = ref false;
     1.8 -fun tracing msg =
     1.9 -  if ! trace
    1.10 +val trace = ref 0;
    1.11 +fun tracing level msg =
    1.12 +  if level <= ! trace
    1.13    then (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
    1.14    else ();
    1.15  
    1.16 @@ -58,10 +58,10 @@
    1.17          else
    1.18            let
    1.19              val timer = Timer.startRealTimer ();
    1.20 -            val _ = tracing (fn () =>
    1.21 +            val _ = tracing 3 (fn () =>
    1.22                "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": waiting");
    1.23              val _ = Mutex.lock critical_lock;
    1.24 -            val _ = tracing (fn () =>
    1.25 +            val _ = tracing 3 (fn () =>
    1.26                "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": passed after " ^
    1.27                Time.toString (Timer.checkRealTimer timer));
    1.28            in () end;
    1.29 @@ -95,9 +95,9 @@
    1.30          val _ =
    1.31            if Mutex.trylock lock then ()
    1.32            else
    1.33 -           (tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting");
    1.34 +           (tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting");
    1.35              Mutex.lock lock;
    1.36 -            tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed"));
    1.37 +            tracing 2 (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed"));
    1.38          val _ = protected_name := name;
    1.39          val res = Exn.capture e ();
    1.40          val _ = protected_name := "";
    1.41 @@ -112,7 +112,7 @@
    1.42      (*the queue of tasks*)
    1.43      val queue = ref tasks;
    1.44      val active = ref 0;
    1.45 -    fun trace_active () = tracing (fn () => "SCHEDULE: " ^ Int.toString (! active) ^ " active");
    1.46 +    fun trace_active () = tracing 1 (fn () => "SCHEDULE: " ^ Int.toString (! active) ^ " active");
    1.47      fun dequeue () =
    1.48        let
    1.49          val (next, tasks') = next_task (! queue);