# HG changeset patch
# User wenzelm
# Date 1280925977 -7200
# Node ID 3342c68d87828a23c2547840fef27e1f1653a1bf
# Parent  c202426474c3985a40f90ceb4d14b6685b43fc7f
schedule_futures: discontinued special treatment of non-parallel proofs, which might have affected memory usage at some point, but does not seem to make a difference with as little as 2GB RAM;

diff -r c202426474c3 -r 3342c68d8782 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 22:28:43 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 04 14:46:17 2010 +0200
@@ -174,8 +174,6 @@
 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   let
     val tasks = Graph.topological_order task_graph;
-    val par_proofs = ! parallel_proofs >= 1;
-
     val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
       (case Graph.get_node task_graph name of
         Task (parents, body) =>
@@ -189,12 +187,8 @@
                 [] => body (map (#1 o Future.join o get) parents)
               | bad => error (loader_msg
                   ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
-            val future' =
-              if par_proofs then future
-              else Future.map (fn (thy, after_load) => (after_load (); (thy, I))) future;
-          in Symtab.update (name, future') tab end
+          in Symtab.update (name, future) tab end
       | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
-
     val _ =
       tasks |> maps (fn name =>
         let