src/Pure/Concurrent/future.ML
changeset 41776 3bd83302a3c3
parent 41737 1b225934c09d
child 42128 eb84d28961a9
equal deleted inserted replaced
41775:6214816d79d3 41776:3bd83302a3c3
   201     val valid = not (Task_Queue.is_canceled group);
   201     val valid = not (Task_Queue.is_canceled group);
   202     val ok =
   202     val ok =
   203       Task_Queue.running task (fn () =>
   203       Task_Queue.running task (fn () =>
   204         setmp_worker_task task (fn () =>
   204         setmp_worker_task task (fn () =>
   205           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
   205           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
   206     val _ = Multithreading.tracing 1 (fn () =>
   206     val _ = Multithreading.tracing 2 (fn () =>
   207       let
   207       let
   208         val s = Task_Queue.str_of_task task;
   208         val s = Task_Queue.str_of_task task;
   209         fun micros time = string_of_int (Time.toNanoseconds time div 1000);
   209         fun micros time = string_of_int (Time.toNanoseconds time div 1000);
   210         val (run, wait, deps) = Task_Queue.timing_of_task task;
   210         val (run, wait, deps) = Task_Queue.timing_of_task task;
   211       in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
   211       in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);