src/Pure/Thy/thy_info.ML
changeset 28449 b6c57eb0fc39
parent 28445 526b8adcd117
child 28533 4e2417eb603e
equal deleted inserted replaced
28448:31a59d7d2168 28449:b6c57eb0fc39
   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)