src/Pure/ML-Systems/multithreading_polyml.ML
changeset 28465 db8667d84dd2
parent 28443 de653f1ad78b
child 28466 6e35fbfc32b8
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 02 19:59:00 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 02 19:59:01 2008 +0200
     1.3 @@ -32,10 +32,11 @@
     1.4  (* options *)
     1.5  
     1.6  val trace = ref 0;
     1.7 +
     1.8  fun tracing level msg =
     1.9 -  if level <= ! trace
    1.10 -  then (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
    1.11 -  else ();
    1.12 +  if level > ! trace then ()
    1.13 +  else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
    1.14 +    handle _ (*sic*) => ();
    1.15  
    1.16  val available = true;
    1.17