# HG changeset patch
# User wenzelm
# Date 1331930421 -3600
# Node ID 9667e0dcb5e24ec17524508e34e97699ba4f6733
# Parent  481b7d9ad6fee22551db76e3a3b6c7834bc9cbd9
check declared vs. defined commands at end of session;

diff -r 481b7d9ad6fe -r 9667e0dcb5e2 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 21:20:23 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 21:40:21 2012 +0100
@@ -12,6 +12,7 @@
   type outer_syntax
   val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
   val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
+  val check_syntax: unit -> unit
   type command_spec = string * Keyword.T
   val command: command_spec -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
@@ -146,6 +147,15 @@
 
 fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
 
+fun check_syntax () =
+  let
+    val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
+  in
+    (case subtract (op =) (map #1 (dest_commands syntax)) major of
+      [] => ()
+    | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
+  end;
+
 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
 
 fun command command_spec comment parse =
diff -r 481b7d9ad6fe -r 9667e0dcb5e2 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Fri Mar 16 21:20:23 2012 +0100
+++ b/src/Pure/System/session.ML	Fri Mar 16 21:40:21 2012 +0100
@@ -75,6 +75,7 @@
 fun finish () =
   (Thy_Info.finish ();
     Present.finish ();
+    Outer_Syntax.check_syntax ();
     Future.shutdown ();
     session_finished := true);