1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 21:20:23 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 21:40:21 2012 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    type outer_syntax
     1.5    val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
     1.6    val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
     1.7 +  val check_syntax: unit -> unit
     1.8    type command_spec = string * Keyword.T
     1.9    val command: command_spec -> string ->
    1.10      (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.11 @@ -146,6 +147,15 @@
    1.12  
    1.13  fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
    1.14  
    1.15 +fun check_syntax () =
    1.16 +  let
    1.17 +    val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
    1.18 +  in
    1.19 +    (case subtract (op =) (map #1 (dest_commands syntax)) major of
    1.20 +      [] => ()
    1.21 +    | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
    1.22 +  end;
    1.23 +
    1.24  fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
    1.25  
    1.26  fun command command_spec comment parse =

     2.1 --- a/src/Pure/System/session.ML	Fri Mar 16 21:20:23 2012 +0100
     2.2 +++ b/src/Pure/System/session.ML	Fri Mar 16 21:40:21 2012 +0100
     2.3 @@ -75,6 +75,7 @@
     2.4  fun finish () =
     2.5    (Thy_Info.finish ();
     2.6      Present.finish ();
     2.7 +    Outer_Syntax.check_syntax ();
     2.8      Future.shutdown ();
     2.9      session_finished := true);
    2.10