equal
deleted
inserted
replaced
318 fun future_schedule task_graph = |
318 fun future_schedule task_graph = |
319 let |
319 let |
320 val tasks = Graph.topological_order task_graph |> map_filter (fn name => |
320 val tasks = Graph.topological_order task_graph |> map_filter (fn name => |
321 (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE)); |
321 (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE)); |
322 |
322 |
|
323 val group = TaskQueue.new_group (); |
323 fun future (name, body) tab = |
324 fun future (name, body) tab = |
324 let |
325 let |
325 val group = TaskQueue.new_group (); |
|
326 val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name); |
326 val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name); |
327 val x = Future.future (SOME group) deps true body; |
327 val x = Future.future (SOME group) deps true body; |
328 in (x, Symtab.update (name, Future.task_of x) tab) end; |
328 in (x, Symtab.update (name, Future.task_of x) tab) end; |
329 in |
329 in |
330 #1 (fold_map future tasks Symtab.empty) |
330 #1 (fold_map future tasks Symtab.empty) |