equal
deleted
inserted
replaced
206 Task_Queue.running task (fn () => |
206 Task_Queue.running task (fn () => |
207 setmp_worker_task task (fn () => |
207 setmp_worker_task task (fn () => |
208 fold (fn job => fn ok => job valid andalso ok) jobs true) ()); |
208 fold (fn job => fn ok => job valid andalso ok) jobs true) ()); |
209 val _ = Multithreading.tracing 2 (fn () => |
209 val _ = Multithreading.tracing 2 (fn () => |
210 let |
210 let |
211 val s = Task_Queue.str_of_task task; |
211 val s = Task_Queue.str_of_task_groups task; |
212 fun micros time = string_of_int (Time.toNanoseconds time div 1000); |
212 fun micros time = string_of_int (Time.toNanoseconds time div 1000); |
213 val (run, wait, deps) = Task_Queue.timing_of_task task; |
213 val (run, wait, deps) = Task_Queue.timing_of_task task; |
214 in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end); |
214 in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end); |
215 val _ = SYNCHRONIZED "finish" (fn () => |
215 val _ = SYNCHRONIZED "finish" (fn () => |
216 let |
216 let |