# HG changeset patch
# User wenzelm
# Date 1222877770 -7200
# Node ID b6c57eb0fc39db8a9b31775b821ea6ce4127418c
# Parent  31a59d7d2168770bfe88a1ac48c07c5a7120f439
future_schedule: back to one group for all loader tasks;

diff -r 31a59d7d2168 -r b6c57eb0fc39 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Oct 01 14:17:06 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Oct 01 18:16:10 2008 +0200
@@ -320,9 +320,9 @@
     val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
       (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
 
+    val group = TaskQueue.new_group ();
     fun future (name, body) tab =
       let
-        val group = TaskQueue.new_group ();
         val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
         val x = Future.future (SOME group) deps true body;
       in (x, Symtab.update (name, Future.task_of x) tab) end;