defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;

--- a/NEWS	Fri Mar 16 13:05:30 2012 +0100
+++ b/NEWS	Fri Mar 16 14:42:11 2012 +0100
@@ -41,6 +41,10 @@
 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
 manual.  Minor INCOMPATIBILITY.
 
+* Forward declaration of outer syntax keywords within the theory
+header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
+commands to be used in the same theory where defined.
+
 
 *** Pure ***
 
@@ -372,9 +376,6 @@
 
 *** ML ***
 
-* Outer syntax keywords for user-defined Isar commands need to be
-defined explicitly in the theory header.  Minor INCOMPATIBILITY.
-
 * Antiquotation @{keyword "name"} produces a parser for outer syntax
 from a minor keyword introduced via theory header declaration.
 

--- a/src/Pure/Isar/toplevel.ML	Fri Mar 16 13:05:30 2012 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Mar 16 14:42:11 2012 +0100
@@ -90,8 +90,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 future list * theory
+  val proof_result: bool -> transition * transition list -> state ->
+    (transition * state) list future * state
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -644,7 +644,7 @@
   in (st', st') end;
 
 
-(* excursion of units, consisting of commands with proof *)
+(* scheduled proof result *)
 
 structure States = Proof_Data
 (
@@ -692,12 +692,4 @@
       in (result, st'') end
   end;
 
-fun excursion input =
-  let
-    val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
-    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 (results, thy) end;
-
 end;

--- a/src/Pure/Thy/thy_load.ML	Fri Mar 16 13:05:30 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Mar 16 14:42:11 2012 +0100
@@ -168,6 +168,26 @@
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;
 
+fun excursion init elements =
+  let
+    val immediate = not (Goal.future_enabled ());
+
+    fun proof_result (tr, trs) (st, _) =
+      let
+        val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
+        val pos' = Toplevel.pos_of (List.last (tr :: trs));
+      in (result, (st', pos')) end;
+
+    fun element_result elem x =
+      fold_map proof_result
+        (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
+
+    val (results, (end_state, end_pos)) =
+      fold_map element_result elements (Toplevel.toplevel, Position.none);
+
+    val thy = Toplevel.end_theory end_pos end_state;
+  in (flat results, thy) end;
+
 fun load_thy update_time dir header pos text parents =
   let
     val time = ! Toplevel.timing;
@@ -179,29 +199,30 @@
       begin_theory dir header parents
       |> Present.begin_theory update_time dir uses;
 
-    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
+    val lexs = Keyword.get_lexicons ();
 
     val toks = Thy_Syntax.parse_tokens lexs pos text;
     val spans = Thy_Syntax.parse_spans toks;
-    val elements =
-      maps (Outer_Syntax.read_element outer_syntax init) (Thy_Syntax.parse_elements spans);
+    val elements = Thy_Syntax.parse_elements spans;
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
+    val (results, thy) = cond_timeit time "" (fn () => excursion init elements);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     val present =
       singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
         deps = map Future.task_of results, pri = 0, interrupts = true})
       (fn () =>
-        Thy_Output.present_thy (#1 lexs) Keyword.command_tags
-          (Outer_Syntax.is_markup outer_syntax)
-          (maps Future.join results) toks
-        |> Buffer.content
-        |> Present.theory_output name);
+        let val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax () in
+          Thy_Output.present_thy minor Keyword.command_tags
+            (Outer_Syntax.is_markup outer_syntax)
+            (maps Future.join results) toks
+          |> Buffer.content
+          |> Present.theory_output name
+        end);
 
   in (thy, present) end;