--- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu Oct 02 19:59:00 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu Oct 02 19:59:01 2008 +0200
@@ -32,10 +32,11 @@
(* options *)
val trace = ref 0;
+
fun tracing level msg =
- if level <= ! trace
- then (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
- else ();
+ if level > ! trace then ()
+ else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
+ handle _ (*sic*) => ();
val available = true;