1.1 --- a/NEWS	Fri Mar 16 13:05:30 2012 +0100
     1.2 +++ b/NEWS	Fri Mar 16 14:42:11 2012 +0100
     1.3 @@ -41,6 +41,10 @@
     1.4  "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
     1.5  manual.  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Forward declaration of outer syntax keywords within the theory
     1.8 +header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
     1.9 +commands to be used in the same theory where defined.
    1.10 +
    1.11  
    1.12  *** Pure ***
    1.13  
    1.14 @@ -372,9 +376,6 @@
    1.15  
    1.16  *** ML ***
    1.17  
    1.18 -* Outer syntax keywords for user-defined Isar commands need to be
    1.19 -defined explicitly in the theory header.  Minor INCOMPATIBILITY.
    1.20 -
    1.21  * Antiquotation @{keyword "name"} produces a parser for outer syntax
    1.22  from a minor keyword introduced via theory header declaration.
    1.23  

     2.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 16 13:05:30 2012 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Mar 16 14:42:11 2012 +0100
     2.3 @@ -90,8 +90,8 @@
     2.4    val add_hook: (transition -> state -> state -> unit) -> unit
     2.5    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     2.6    val command: transition -> state -> state
     2.7 -  val excursion:
     2.8 -    (transition * transition list) list -> (transition * state) list future list * theory
     2.9 +  val proof_result: bool -> transition * transition list -> state ->
    2.10 +    (transition * state) list future * state
    2.11  end;
    2.12  
    2.13  structure Toplevel: TOPLEVEL =
    2.14 @@ -644,7 +644,7 @@
    2.15    in (st', st') end;
    2.16  
    2.17  
    2.18 -(* excursion of units, consisting of commands with proof *)
    2.19 +(* scheduled proof result *)
    2.20  
    2.21  structure States = Proof_Data
    2.22  (
    2.23 @@ -692,12 +692,4 @@
    2.24        in (result, st'') end
    2.25    end;
    2.26  
    2.27 -fun excursion input =
    2.28 -  let
    2.29 -    val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
    2.30 -    val immediate = not (Goal.future_enabled ());
    2.31 -    val (results, end_state) = fold_map (proof_result immediate) input toplevel;
    2.32 -    val thy = end_theory end_pos end_state;
    2.33 -  in (results, thy) end;
    2.34 -
    2.35  end;

     3.1 --- a/src/Pure/Thy/thy_load.ML	Fri Mar 16 13:05:30 2012 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Mar 16 14:42:11 2012 +0100
     3.3 @@ -168,6 +168,26 @@
     3.4    |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
     3.5    |> Theory.checkpoint;
     3.6  
     3.7 +fun excursion init elements =
     3.8 +  let
     3.9 +    val immediate = not (Goal.future_enabled ());
    3.10 +
    3.11 +    fun proof_result (tr, trs) (st, _) =
    3.12 +      let
    3.13 +        val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
    3.14 +        val pos' = Toplevel.pos_of (List.last (tr :: trs));
    3.15 +      in (result, (st', pos')) end;
    3.16 +
    3.17 +    fun element_result elem x =
    3.18 +      fold_map proof_result
    3.19 +        (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
    3.20 +
    3.21 +    val (results, (end_state, end_pos)) =
    3.22 +      fold_map element_result elements (Toplevel.toplevel, Position.none);
    3.23 +
    3.24 +    val thy = Toplevel.end_theory end_pos end_state;
    3.25 +  in (flat results, thy) end;
    3.26 +
    3.27  fun load_thy update_time dir header pos text parents =
    3.28    let
    3.29      val time = ! Toplevel.timing;
    3.30 @@ -179,29 +199,30 @@
    3.31        begin_theory dir header parents
    3.32        |> Present.begin_theory update_time dir uses;
    3.33  
    3.34 -    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
    3.35 +    val lexs = Keyword.get_lexicons ();
    3.36  
    3.37      val toks = Thy_Syntax.parse_tokens lexs pos text;
    3.38      val spans = Thy_Syntax.parse_spans toks;
    3.39 -    val elements =
    3.40 -      maps (Outer_Syntax.read_element outer_syntax init) (Thy_Syntax.parse_elements spans);
    3.41 +    val elements = Thy_Syntax.parse_elements spans;
    3.42  
    3.43      val _ = Present.theory_source name
    3.44        (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    3.45  
    3.46      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    3.47 -    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
    3.48 +    val (results, thy) = cond_timeit time "" (fn () => excursion init elements);
    3.49      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    3.50  
    3.51      val present =
    3.52        singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
    3.53          deps = map Future.task_of results, pri = 0, interrupts = true})
    3.54        (fn () =>
    3.55 -        Thy_Output.present_thy (#1 lexs) Keyword.command_tags
    3.56 -          (Outer_Syntax.is_markup outer_syntax)
    3.57 -          (maps Future.join results) toks
    3.58 -        |> Buffer.content
    3.59 -        |> Present.theory_output name);
    3.60 +        let val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax () in
    3.61 +          Thy_Output.present_thy minor Keyword.command_tags
    3.62 +            (Outer_Syntax.is_markup outer_syntax)
    3.63 +            (maps Future.join results) toks
    3.64 +          |> Buffer.content
    3.65 +          |> Present.theory_output name
    3.66 +        end);
    3.67  
    3.68    in (thy, present) end;
    3.69