merged

--- a/src/Pure/Isar/outer_syntax.ML	Sat Jan 10 15:55:19 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Jan 10 16:00:34 2009 +0100
@@ -32,7 +32,7 @@
   type isar
   val isar: bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
-  val load_thy: string -> Position.T -> string list -> bool -> unit
+  val load_thy: string -> Position.T -> string list -> bool -> unit -> unit
 end;
 
 structure OuterSyntax: OUTER_SYNTAX =
@@ -288,16 +288,13 @@
       (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val _ = cond_timeit time "" (fn () =>
-      let
-        val (results, commit_exit) = Toplevel.excursion units;
-        val _ =
-          ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup results toks
-          |> Buffer.content
-          |> Present.theory_output name
-        val _ = commit_exit ();
-      in () end);
+    val results = cond_timeit time "" (fn () => Toplevel.excursion units);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
-  in () end;
+
+    fun after_load () =
+      ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (Lazy.force results) toks
+      |> Buffer.content
+      |> Present.theory_output name;
+  in after_load end;
 
 end;

--- a/src/Pure/Isar/toplevel.ML	Sat Jan 10 15:55:19 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Jan 10 16:00:34 2009 +0100
@@ -96,7 +96,7 @@
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val commit_exit: Position.T -> transition
   val command: transition -> state -> state
-  val excursion: (transition * transition list) list -> (transition * state) list * (unit -> unit)
+  val excursion: (transition * transition list) list -> (transition * state) list lazy
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -746,12 +746,12 @@
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
     val immediate = not (Future.enabled ());
-    val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
+    val (results, end_state) = fold_map (proof_result immediate) input toplevel;
     val _ =
       (case end_state of
-        State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
+        State (NONE, SOME (Theory (Context.Theory _, _), _)) =>
+          command (commit_exit end_pos) end_state
       | _ => error "Unfinished development at end of input");
-    val results = maps Lazy.force future_results;
-  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
+  in Lazy.lazy (fn () => maps Lazy.force results) end;
 
 end;

--- a/src/Pure/Thy/thy_info.ML	Sat Jan 10 15:55:19 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Jan 10 16:00:34 2009 +0100
@@ -243,14 +243,6 @@
 
 val kill_thy = if_known_thy remove_thy;
 
-fun consolidate_thy name =
-  (case lookup_theory name of
-    NONE => []
-  | SOME thy =>
-      (case PureThy.join_proofs thy of
-        [] => []
-      | exns => (kill_thy name; exns)));
-
 
 (* load_file *)
 
@@ -320,33 +312,29 @@
     val _ = CRITICAL (fn () =>
       change_deps name (Option.map (fn {master, text, parents, files, ...} =>
         make_deps upd_time master text parents files)));
-    val _ = OuterSyntax.load_thy name pos text (time orelse ! Output.timing);
-  in
-    CRITICAL (fn () =>
-     (change_deps name
-        (Option.map (fn {update_time, master, parents, files, ...} =>
-          make_deps update_time master [] parents files));
-      perform Update name))
-  end;
+    val after_load = OuterSyntax.load_thy name pos text (time orelse ! Output.timing);
+    val _ =
+      CRITICAL (fn () =>
+       (change_deps name
+          (Option.map (fn {update_time, master, parents, files, ...} =>
+            make_deps update_time master [] parents files));
+        perform Update name));
+  in after_load end;
 
 
 (* scheduling loader tasks *)
 
-datatype task = Task of (unit -> unit) | Finished | Running;
+datatype task = Task of (unit -> unit -> unit) | Finished | Running;
 fun task_finished Finished = true | task_finished _ = false;
 
 local
 
-fun schedule_seq tasks =
-  Graph.topological_order tasks
-  |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
-
 fun schedule_futures task_graph =
   let
     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));
 
-    fun future (name, body) tab =
+    fun fork (name, body) tab =
       let
         val deps = Graph.imm_preds task_graph name
           |> map_filter (fn parent =>
@@ -358,12 +346,23 @@
             [] => body ()
           | bad => error (loader_msg
               ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
+      in Symtab.update (name, x) tab end;
 
-      in (x, Symtab.update (name, x) tab) end;
+    val futures = fold fork tasks Symtab.empty;
 
-    val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
-    val proof_results = map Exn.Exn (maps (consolidate_thy o #1) tasks);
-  in ignore (Exn.release_all (thy_results @ proof_results)) end;
+    val exns = tasks |> maps (fn (name, _) =>
+      let
+        val after_load = Future.join (the (Symtab.lookup futures name));
+        val _ = after_load ();
+        val proof_exns = PureThy.join_proofs (get_theory name);
+        val _ = null proof_exns orelse raise Exn.EXCEPTIONS proof_exns;
+      in [] end handle exn => (kill_thy name; [exn]));
+
+  in ignore (Exn.release_all (map Exn.Exn exns)) end;
+
+fun schedule_seq tasks =
+  Graph.topological_order tasks
+  |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ()));
 
 in