1.1 --- a/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 15:28:48 2011 +0100
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 16:34:10 2011 +0100
     1.3 @@ -10,6 +10,9 @@
     1.4    val dummy_task: task
     1.5    val pri_of_task: task -> int
     1.6    val str_of_task: task -> string
     1.7 +  val timing_of_task: task -> Time.time * Time.time
     1.8 +  val running: task -> (unit -> 'a) -> 'a
     1.9 +  val waiting: task -> (unit -> 'a) -> 'a
    1.10    type group
    1.11    val new_group: group option -> group
    1.12    val group_id: group -> int
    1.13 @@ -41,18 +44,40 @@
    1.14  val new_id = Synchronized.counter ();
    1.15  
    1.16  
    1.17 +(* timing *)
    1.18 +
    1.19 +type timing = Time.time * Time.time;
    1.20 +
    1.21 +fun new_timing () =
    1.22 +  Synchronized.var "Task_Queue.timing" (Time.zeroTime, Time.zeroTime);
    1.23 +
    1.24 +fun gen_timing which timing e =
    1.25 +  let
    1.26 +    val start = Time.now ();
    1.27 +    val result = Exn.capture e ();
    1.28 +    val t = Time.- (Time.now (), start);
    1.29 +    val _ = Synchronized.change timing (which (fn t' => Time.+ (t, t')));
    1.30 +  in Exn.release result end;
    1.31 +
    1.32 +
    1.33  (* tasks *)
    1.34  
    1.35 -abstype task = Task of int option * int
    1.36 +abstype task = Task of (int option * int) * timing Synchronized.var
    1.37  with
    1.38  
    1.39 -val dummy_task = Task (NONE, ~1);
    1.40 -fun new_task pri = Task (pri, new_id ());
    1.41 +val dummy_task = Task ((NONE, ~1), new_timing ());
    1.42 +fun new_task pri = Task ((pri, new_id ()), new_timing ());
    1.43  
    1.44 -fun pri_of_task (Task (pri, _)) = the_default 0 pri;
    1.45 -fun str_of_task (Task (_, i)) = string_of_int i;
    1.46 +fun pri_of_task (Task ((pri, _), _)) = the_default 0 pri;
    1.47 +fun str_of_task (Task ((_, i), _)) = string_of_int i;
    1.48  
    1.49 -fun task_ord (Task t1, Task t2) = prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2);
    1.50 +fun timing_of_task (Task (_, timing)) = Synchronized.value timing;
    1.51 +fun running (Task (_, timing)) = gen_timing apfst timing;
    1.52 +fun waiting (Task (_, timing)) = gen_timing apsnd timing;
    1.53 +
    1.54 +fun task_ord (Task (t1, _), Task (t2, _)) =
    1.55 +  prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2);
    1.56 +
    1.57  val eq_task = is_equal o task_ord;
    1.58  
    1.59  end;