src/Doc/antiquote_setup.ML
changeset 53061 417cb0f713e0
parent 53045 4c297ee47c28
child 54372 2d61935eed4a
     1.1 --- a/src/Doc/antiquote_setup.ML	Sun Aug 18 13:28:06 2013 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Aug 18 13:58:33 2013 +0200
     1.3 @@ -146,6 +146,16 @@
     1.4  
     1.5  fun no_check _ _ = true;
     1.6  
     1.7 +fun command_check (name, pos) =
     1.8 +  is_some (Keyword.command_keyword name) andalso
     1.9 +    let
    1.10 +      val markup =
    1.11 +        Outer_Syntax.scan Position.none name
    1.12 +        |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
    1.13 +        |> map (snd o fst);
    1.14 +      val _ = List.app (Position.report pos) markup;
    1.15 +    in true end;
    1.16 +
    1.17  fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
    1.18  
    1.19  fun check_tool (name, pos) =
    1.20 @@ -199,7 +209,7 @@
    1.21  
    1.22  val entity_setup =
    1.23    entity_antiqs no_check "" "syntax" #>
    1.24 -  entity_antiqs (K (is_some o Keyword.command_keyword o #1)) "isacommand" "command" #>
    1.25 +  entity_antiqs (K command_check) "isacommand" "command" #>
    1.26    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
    1.27    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
    1.28    entity_antiqs (thy_check Method.check) "" "method" #>