src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -31,7 +31,7 @@
   type isar
   val isar: bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
-  val load_thy: string -> Position.T -> string -> (unit -> unit) * theory
+  val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -249,9 +249,9 @@
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
-fun prepare_unit commands (cmd, proof, proper_proof) =
+fun prepare_unit commands init (cmd, proof, proper_proof) =
   let
-    val (tr, proper_cmd) = prepare_span commands cmd;
+    val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
     val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
   in
     if proper_cmd andalso proper_proof then [(tr, proof_trs)]
@@ -268,7 +268,7 @@
 
 (* load_thy *)
 
-fun load_thy name pos text =
+fun load_thy name init pos text =
   let
     val (lexs, commands) = get_syntax ();
     val time = ! Output.timing;
@@ -279,7 +279,7 @@
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
     val _ = List.app Thy_Syntax.report_span spans;
     val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
-      |> Par_List.map (prepare_unit commands) |> flat;
+      |> Par_List.map (prepare_unit commands init) |> flat;
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);