more thorough check_command, including completion;

--- a/src/Doc/antiquote_setup.ML	Tue Nov 10 20:10:17 2015 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Nov 10 20:49:48 2015 +0100
@@ -150,20 +150,7 @@
 fun is_keyword ctxt (name, _) =
   Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name;
 
-fun check_command ctxt (name, pos) =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val keywords = Thy_Header.get_keywords thy;
-  in
-    Keyword.is_command keywords name andalso
-      let
-        val markup =
-          Token.explode keywords Position.none name
-          |> maps (Outer_Syntax.command_reports thy)
-          |> map (snd o fst);
-        val _ = Context_Position.reports ctxt (map (pair pos) markup);
-      in true end
-  end;
+fun check_command ctxt (name, pos) = (Outer_Syntax.check_command ctxt (name, pos); true);
 
 fun check_system_option ctxt (name, pos) =
   (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)

--- a/src/Pure/Isar/keyword.ML	Tue Nov 10 20:10:17 2015 +0100
+++ b/src/Pure/Isar/keyword.ML	Tue Nov 10 20:49:48 2015 +0100
@@ -43,6 +43,7 @@
   val is_keyword: keywords -> string -> bool
   val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
+  val dest_commands: keywords -> string list
   val command_markup: keywords -> string -> Markup.T option
   val command_kind: keywords -> string -> string option
   val command_files: keywords -> string -> Path.T -> Path.T list
@@ -187,6 +188,8 @@
 fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
 fun is_literal keywords = is_keyword keywords orf is_command keywords;
 
+fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands;
+
 
 (* command keywords *)
 

--- a/src/Pure/Isar/outer_syntax.ML	Tue Nov 10 20:10:17 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Nov 10 20:49:48 2015 +0100
@@ -25,6 +25,7 @@
   val parse_spans: Token.T list -> Command_Span.span list
   val side_comments: Token.T list -> Token.T list
   val command_reports: theory -> Token.T -> Position.report_text list
+  val check_command: Proof.context -> string * Position.T -> string
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -268,7 +269,7 @@
 val side_comments = filter Token.is_proper #> cmts;
 
 
-(* read commands *)
+(* check commands *)
 
 fun command_reports thy tok =
   if Token.is_command tok then
@@ -279,4 +280,30 @@
     end
   else [];
 
+fun check_command ctxt (name, pos) =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val keywords = Thy_Header.get_keywords thy;
+  in
+    if Keyword.is_command keywords name then
+      let
+        val markup =
+          Token.explode keywords Position.none name
+          |> maps (command_reports thy)
+          |> map (#2 o #1);
+        val _ = Context_Position.reports ctxt (map (pair pos) markup);
+      in name end
+    else
+      let
+        val completion =
+          Completion.make (name, pos)
+            (fn completed =>
+              Keyword.dest_commands keywords
+              |> filter completed
+              |> sort_strings
+              |> map (fn a => (a, (Markup.commandN, a))));
+        val report = Markup.markup_report (Completion.reported_text completion);
+      in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end
+  end;
+
 end;