# HG changeset patch
# User wenzelm
# Date 1185744460 -7200
# Node ID 8a15a04e36f68985d59685d2c96c17cfca42e392
# Parent  245b7e68a3bc91ed78681659e7859fe5e3949c83
tuned msgs;
tuned;

diff -r 245b7e68a3bc -r 8a15a04e36f6 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 22:42:02 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jul 29 23:27:40 2007 +0200
@@ -10,6 +10,9 @@
 structure Multithreading: MULTITHREADING =
 struct
 
+
+(* flags *)
+
 val trace = ref false;
 fun tracing msg =
   if ! trace
@@ -20,16 +23,22 @@
 val max_threads = ref 1;
 
 
+(* misc utils *)
+
+fun show "" = ""
+  | show name = " " ^ name;
+
+fun show' "" = ""
+  | show' name = " [" ^ name ^ "]";
+
+fun inc i = (i := ! i + 1; ! i);
+fun dec i = (i := ! i - 1; ! i);
+
+
 (* critical section -- may be nested within the same thread *)
 
 local
 
-fun add_name "" = ""
-  | add_name name = " " ^ name;
-
-fun add_name' "" = ""
-  | add_name' name = " [" ^ name ^ "]";
-
 val critical_lock = Mutex.mutex ();
 val critical_thread = ref (NONE: Thread.thread option);
 val critical_name = ref "";
@@ -51,10 +60,10 @@
           let
             val timer = Timer.startRealTimer ();
             val _ = tracing (fn () =>
-              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": waiting for lock");
+              "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": waiting");
             val _ = Mutex.lock critical_lock;
             val _ = tracing (fn () =>
-              "CRITICAL" ^ add_name name ^ add_name' (! critical_name) ^ ": obtained lock after " ^
+              "CRITICAL" ^ show name ^ show' (! critical_name) ^ ": passed after " ^
               Time.toString (Timer.checkRealTimer timer));
           in () end;
       val _ = critical_thread := SOME (Thread.self ());
@@ -72,8 +81,11 @@
 
 (* scheduling -- non-interruptible threads working on a queue of tasks *)
 
-fun inc i = (i := ! i + 1; ! i);
-fun dec i = (i := ! i - 1; ! i);
+local
+
+val protected_name = ref "";
+
+in
 
 fun schedule n next_task tasks =
   let
@@ -84,10 +96,12 @@
         val _ =
           if Mutex.trylock lock then ()
           else
-           (tracing (fn () => "PROTECTED " ^ name ^ ": waiting for lock");
+           (tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": waiting");
             Mutex.lock lock;
-            tracing (fn () => "PROTECTED " ^ name ^ ": obtained lock"));
+            tracing (fn () => "PROTECTED" ^ show name ^ show' (! protected_name) ^ ": passed"));
+        val _ = protected_name := name;
         val res = Exn.capture e ();
+        val _ = protected_name := "";
         val _ = Mutex.unlock lock;
       in Exn.release res end;
 
@@ -140,5 +154,7 @@
 
 end;
 
+end;
+
 val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
 val CRITICAL = Multithreading.CRITICAL;