refined task timing: joining vs. waiting;
tuned;

--- a/src/Pure/Concurrent/future.ML	Tue Feb 01 19:39:26 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 01 21:05:22 2011 +0100
@@ -38,7 +38,6 @@
   val worker_task: unit -> Task_Queue.task option
   val worker_group: unit -> Task_Queue.group option
   val worker_subgroup: unit -> Task_Queue.group
-  val worker_waiting: (unit -> 'a) -> 'a
   type 'a future
   val task_of: 'a future -> task
   val group_of: 'a future -> group
@@ -87,6 +86,11 @@
 val worker_group = Option.map #2 o thread_data;
 fun worker_subgroup () = Task_Queue.new_group (worker_group ());
 
+fun worker_joining e =
+  (case worker_task () of
+    NONE => e ()
+  | SOME task => Task_Queue.joining task e);
+
 fun worker_waiting e =
   (case worker_task () of
     NONE => e ()
@@ -449,11 +453,11 @@
   else
     (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
       (NONE, []) => NONE
-    | (NONE, deps') => (worker_wait true work_finished; join_next deps')
+    | (NONE, deps') => (worker_waiting (fn () => worker_wait true work_finished); join_next deps')
     | (SOME work, deps') => SOME (work, deps'));
 
 fun execute_work NONE = ()
-  | execute_work (SOME (work, deps')) = (execute work; join_work deps')
+  | execute_work (SOME (work, deps')) = (worker_joining (fn () => execute work); join_work deps')
 and join_work deps =
   execute_work (SYNCHRONIZED "join" (fn () => join_next deps));
 
@@ -464,15 +468,16 @@
 in
 
 fun join_results xs =
-  if forall is_finished xs then map get_result xs
-  else if Multithreading.self_critical () then
-    error "Cannot join future values within critical section"
-  else
-    worker_waiting (fn () =>
-      (case worker_task () of
-        SOME task => join_depend task (map task_of xs)
-      | NONE => List.app (ignore o Single_Assignment.await o result_of) xs;
-      map get_result xs));
+  let
+    val _ =
+      if forall is_finished xs then ()
+      else if Multithreading.self_critical () then
+        error "Cannot join future values within critical section"
+      else
+        (case worker_task () of
+          SOME task => join_depend task (map task_of xs)
+        | NONE => List.app (ignore o Single_Assignment.await o result_of) xs);
+  in map get_result xs end;
 
 end;
 

--- a/src/Pure/Concurrent/task_queue.ML	Tue Feb 01 19:39:26 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Feb 01 21:05:22 2011 +0100
@@ -12,6 +12,7 @@
   val str_of_task: task -> string
   val timing_of_task: task -> Time.time * Time.time
   val running: task -> (unit -> 'a) -> 'a
+  val joining: task -> (unit -> 'a) -> 'a
   val waiting: task -> (unit -> 'a) -> 'a
   type group
   val new_group: group option -> group
@@ -50,14 +51,14 @@
 type timing = Time.time * Time.time;
 
 fun new_timing () =
-  Synchronized.var "Task_Queue.timing" (Time.zeroTime, Time.zeroTime);
+  Synchronized.var "timing" (Time.zeroTime, Time.zeroTime);
 
-fun gen_timing which timing e =
+fun gen_timing account timing e =
   let
     val start = Time.now ();
     val result = Exn.capture e ();
     val t = Time.- (Time.now (), start);
-    val _ = Synchronized.change timing (which (fn t' => Time.+ (t, t')));
+    val _ = Synchronized.change timing (account t);
   in Exn.release result end;
 
 
@@ -78,8 +79,11 @@
   if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
 
 fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
-fun running (Task {timing, ...}) = gen_timing apfst timing;
-fun waiting (Task {timing, ...}) = gen_timing apsnd timing;
+
+fun running (Task {timing, ...}) = gen_timing (fn t => fn (a, b) => (Time.+ (a, t), b)) timing;
+fun joining (Task {timing, ...}) = gen_timing (fn t => fn (a, b) => (Time.- (a, t), b)) timing;
+fun waiting (Task {timing, ...}) =
+  gen_timing (fn t => fn (a, b) => (Time.- (a, t), Time.+ (b, t))) timing;
 
 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));