# HG changeset patch
# User wenzelm
# Date 1231628171 -3600
# Node ID a96236886804a65992cad318cfdbfa7f884e40de
# Parent  dc6b19966757a36ee7f6b065ebc32b23798ff0dc
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;

diff -r dc6b19966757 -r a96236886804 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Jan 10 21:47:02 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Jan 10 23:56:11 2009 +0100
@@ -350,6 +350,8 @@
     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 par_proofs = ! parallel_proofs;
+
     fun fork (name, body) tab =
       let
         val deps = Graph.imm_preds task_graph name
@@ -357,12 +359,15 @@
             (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
         fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
 
-        val x = Future.fork_deps (map #2 deps) (fn () =>
+        val future = Future.fork_deps (map #2 deps) (fn () =>
           (case map_filter failed deps of
             [] => body ()
           | bad => error (loader_msg
               ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
-      in Symtab.update (name, x) tab end;
+        val future' =
+          if par_proofs then future
+          else Future.map (fn after_load => (after_load (); fn () => ())) future;
+      in Symtab.update (name, future') tab end;
 
     val futures = fold fork tasks Symtab.empty;