present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;

--- a/src/Pure/Isar/outer_syntax.ML	Sat Mar 26 21:28:04 2011 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Mar 26 21:45:29 2011 +0100
@@ -31,7 +31,7 @@
   type isar
   val isar: TextIO.instream -> bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
-  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> (unit -> unit) * theory
+  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> theory * unit future
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -288,11 +288,16 @@
     val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
-    fun after_load () =
-      Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
-      |> Buffer.content
-      |> Present.theory_output name;
-  in (after_load, thy) end;
+    val present =
+      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
+        deps = map Future.task_of results, pri = 0})
+      (fn () =>
+        Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup
+          (maps Future.join results) toks
+        |> Buffer.content
+        |> Present.theory_output name);
+
+  in (thy, present) end;
 
 end;
 

--- a/src/Pure/Isar/toplevel.ML	Sat Mar 26 21:28:04 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Mar 26 21:45:29 2011 +0100
@@ -89,7 +89,8 @@
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
-  val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
+  val excursion:
+    (transition * transition list) list -> (transition * state) list future list * theory
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -655,7 +656,7 @@
       Proof.is_relevant (proof_of st')
     then
       let val (states, st'') = fold_map command_result proof_trs st'
-      in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end
+      in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end
     else
       let
         val (body_trs, end_tr) = split_last proof_trs;
@@ -679,8 +680,8 @@
           (case States.get (presentation_context_of st'') of
             NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
           | SOME states => states);
-        val result = Lazy.lazy
-          (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
+        val result = states
+          |> Future.map (fn sts => (tr, st') :: (body_trs ~~ sts) @ [(end_tr, st'')]);
 
       in (result, st'') end
   end;
@@ -691,6 +692,6 @@
     val immediate = not (Goal.future_enabled ());
     val (results, end_state) = fold_map (proof_result immediate) input toplevel;
     val thy = end_theory end_pos end_state;
-  in (Lazy.lazy (fn () => maps Lazy.force results), thy) end;
+  in (results, thy) end;
 
 end;

--- a/src/Pure/Thy/thy_info.ML	Sat Mar 26 21:28:04 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Mar 26 21:45:29 2011 +0100
@@ -155,7 +155,7 @@
 (* scheduling loader tasks *)
 
 datatype task =
-  Task of string list * (theory list -> (theory * (unit -> unit))) |
+  Task of string list * (theory list -> (theory * unit future * (unit -> unit))) |
   Finished of theory;
 
 fun task_finished (Task _) = false
@@ -168,8 +168,9 @@
     (case Graph.get_node task_graph name of
       Task (parents, body) =>
         let
-          val (thy, after_load) = body (map (the o Symtab.lookup tab) parents);
-          val _ = after_load ();
+          val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents);
+          val _ = Future.join present;
+          val _ = commit ();
         in Symtab.update (name, thy) tab end
     | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
 
@@ -194,13 +195,14 @@
                   | bad => error (loader_msg ("failed to load " ^ quote name ^
                       " (unresolved " ^ commas_quote bad ^ ")") [])));
           in Symtab.update (name, future) tab end
-      | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
+      | Finished thy => Symtab.update (name, Future.value (thy, Future.value (), I)) tab));
     val _ =
       tasks |> maps (fn name =>
         let
-          val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
+          val (thy, present, commit) = Future.join (the (Symtab.lookup futures name));
           val _ = Global_Theory.join_proofs thy;
-          val _ = after_load ();
+          val _ = Future.join present;
+          val _ = commit ();
         in [] end handle exn => [Exn.Exn exn])
       |> rev |> Exn.release_all;
   in () end) ();
@@ -237,17 +239,15 @@
       Thy_Load.begin_theory dir name imports parent_thys uses
       |> Present.begin_theory update_time dir uses;
 
-    val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
+    val (theory, present) = Outer_Syntax.load_thy name init pos text;
 
     val parents = map Context.theory_name parent_thys;
-    fun after_load' () =
-     (after_load ();
+    fun commit () =
       NAMED_CRITICAL "Thy_Info" (fn () =>
        (map get_theory parents;
         change_thys (new_entry name parents (SOME deps, SOME theory));
-        perform Update name)));
-
-  in (theory, after_load') end;
+        perform Update name));
+  in (theory, present, commit) end;
 
 fun check_deps dir name =
   (case lookup_deps name of
@@ -255,7 +255,7 @@
   | NONE =>
       let val {master, text, imports, ...} = Thy_Load.check_thy dir name
       in (false, SOME (make_deps master imports, text), imports) end
-  | SOME (SOME {master, imports}) =>
+  | SOME (SOME {master, ...}) =>
       let
         val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name;
         val deps' = SOME (make_deps master' imports', text');