# HG changeset patch
# User wenzelm
# Date 1231589438 -3600
# Node ID 3ab54b42ded80eb166e83da4e46e0f05ffa1b8f0
# Parent  7ba952481e29f4b1c214b799e71f55050c47d393
load_thy: explicit after_load phase for presentation;

diff -r 7ba952481e29 -r 3ab54b42ded8 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Jan 10 13:10:07 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Jan 10 13:10:38 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;