# HG changeset patch
# User wenzelm
# Date 1222522621 -7200
# Node ID 0130201cc0e3e37dd9a4da792181b8dee399cac3
# Parent  0de8a35b866a29df799078cb351a4b4f0e290f2e
more tracing;

diff -r 0de8a35b866a -r 0130201cc0e3 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Sep 27 15:20:39 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Sep 27 15:37:01 2008 +0200
@@ -95,12 +95,12 @@
 
 fun SYNCHRONIZED name e = uninterruptible (fn restore_attributes => fn () =>
   let
-    val _ = Multithreading.tracing 4 (fn () => name ^ ": locking");
+    val _ = Multithreading.tracing 3 (fn () => name ^ ": locking");
     val _ = Mutex.lock lock;
-    val _ = Multithreading.tracing 4 (fn () => name ^ ": locked");
+    val _ = Multithreading.tracing 3 (fn () => name ^ ": locked");
     val result = Exn.capture (restore_attributes e) ();
     val _ = Mutex.unlock lock;
-    val _ = Multithreading.tracing 4 (fn () => name ^ ": unlocked");
+    val _ = Multithreading.tracing 3 (fn () => name ^ ": unlocked");
   in Exn.release result end) ();
 
 fun wait name = (*requires SYNCHRONIZED*)
@@ -120,9 +120,9 @@
 fun execute name (task, group, run) =
   let
     val _ = set_thread_data (SOME (task, group));
-    val _ = Multithreading.tracing 4 (fn () => name ^ ": running");
+    val _ = Multithreading.tracing 3 (fn () => name ^ ": running");
     val ok = run ();
-    val _ = Multithreading.tracing 4 (fn () => name ^ ": finished");
+    val _ = Multithreading.tracing 3 (fn () => name ^ ": finished");
     val _ = set_thread_data NONE;
     val _ = SYNCHRONIZED "execute" (fn () =>
      (change queue (TaskQueue.finish task);
@@ -160,7 +160,7 @@
 
 fun worker_loop name =
   (case SYNCHRONIZED name (fn () => worker_next name) of
-    NONE => Multithreading.tracing 4 (fn () => name ^ ": exit")
+    NONE => Multithreading.tracing 3 (fn () => name ^ ": exit")
   | SOME work => (execute name work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
@@ -199,7 +199,7 @@
 
 fun scheduler_loop () =
  (while SYNCHRONIZED "scheduler" scheduler_next do ();
-  Multithreading.tracing 4 (fn () => "scheduler: exit"));
+  Multithreading.tracing 3 (fn () => "scheduler: exit"));
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);