src/Pure/Concurrent/future.ML
changeset 44823 804783d6ee26
parent 44633 e72ba84ae58f
child 44824 318ca53e3fbb
     1.1 --- a/src/Pure/Concurrent/future.ML	Sat Jul 23 20:34:33 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sat Jul 23 21:29:56 2011 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4            fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     1.5      val _ = Multithreading.tracing 2 (fn () =>
     1.6        let
     1.7 -        val s = Task_Queue.str_of_task task;
     1.8 +        val s = Task_Queue.str_of_task_groups task;
     1.9          fun micros time = string_of_int (Time.toNanoseconds time div 1000);
    1.10          val (run, wait, deps) = Task_Queue.timing_of_task task;
    1.11        in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);