future_schedule: back to one group for all loader tasks;
authorwenzelm
Wed Oct 01 18:16:10 2008 +0200 (2008-10-01)
changeset 28449b6c57eb0fc39
parent 28448 31a59d7d2168
child 28450 504c4edead13
future_schedule: back to one group for all loader tasks;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Oct 01 14:17:06 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Oct 01 18:16:10 2008 +0200
     1.3 @@ -320,9 +320,9 @@
     1.4      val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
     1.5        (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
     1.6  
     1.7 +    val group = TaskQueue.new_group ();
     1.8      fun future (name, body) tab =
     1.9        let
    1.10 -        val group = TaskQueue.new_group ();
    1.11          val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
    1.12          val x = Future.future (SOME group) deps true body;
    1.13        in (x, Symtab.update (name, Future.task_of x) tab) end;