Task_Queue.update_timing: more precise treatment of interruptibility;
Task_Queue.waiting: potentially expensive wait dependencies are subject to trace flag;

--- a/src/Pure/Concurrent/task_queue.ML	Fri Feb 04 16:29:47 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Feb 04 16:33:12 2011 +0100
@@ -120,12 +120,13 @@
 fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
 
 fun update_timing update (Task {timing, ...}) e =
-  let
-    val start = Time.now ();
-    val result = Exn.capture e ();
-    val t = Time.- (Time.now (), start);
-    val _ = Synchronized.change timing (update t);
-  in Exn.release result end;
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val start = Time.now ();
+      val result = Exn.capture (restore_attributes e) ();
+      val t = Time.- (Time.now (), start);
+      val _ = Synchronized.change timing (update t);
+    in Exn.release result end) ();
 
 fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
   prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
@@ -147,7 +148,9 @@
 
 fun waiting task deps =
   update_timing (fn t => fn (a, b, ds) =>
-    (Time.- (a, t), Time.+ (b, t), fold (insert (op =) o name_of_task) deps ds)) task;
+    (Time.- (a, t), Time.+ (b, t),
+      if ! Multithreading.trace > 0
+      then fold (insert (op =) o name_of_task) deps ds else ds)) task;