# HG changeset patch
# User wenzelm
# Date 1376827113 -7200
# Node ID 417cb0f713e0c556e67809c7727fef0fe6bee95e
# Parent  444ee65295748d33df64fb3d00de4dc1362b107a
more markup;

diff -r 444ee6529574 -r 417cb0f713e0 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Aug 18 13:28:06 2013 +0200
+++ b/src/Doc/antiquote_setup.ML	Sun Aug 18 13:58:33 2013 +0200
@@ -146,6 +146,16 @@
 
 fun no_check _ _ = true;
 
+fun command_check (name, pos) =
+  is_some (Keyword.command_keyword name) andalso
+    let
+      val markup =
+        Outer_Syntax.scan Position.none name
+        |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
+        |> map (snd o fst);
+      val _ = List.app (Position.report pos) markup;
+    in true end;
+
 fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
 
 fun check_tool (name, pos) =
@@ -199,7 +209,7 @@
 
 val entity_setup =
   entity_antiqs no_check "" "syntax" #>
-  entity_antiqs (K (is_some o Keyword.command_keyword o #1)) "isacommand" "command" #>
+  entity_antiqs (K command_check) "isacommand" "command" #>
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
   entity_antiqs (thy_check Method.check) "" "method" #>