src/Doc/antiquote_setup.ML
changeset 53061 417cb0f713e0
parent 53045 4c297ee47c28
child 54372 2d61935eed4a
equal deleted inserted replaced
53060:444ee6529574 53061:417cb0f713e0
   143 (* Isabelle/Isar entities (with index) *)
   143 (* Isabelle/Isar entities (with index) *)
   144 
   144 
   145 local
   145 local
   146 
   146 
   147 fun no_check _ _ = true;
   147 fun no_check _ _ = true;
       
   148 
       
   149 fun command_check (name, pos) =
       
   150   is_some (Keyword.command_keyword name) andalso
       
   151     let
       
   152       val markup =
       
   153         Outer_Syntax.scan Position.none name
       
   154         |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
       
   155         |> map (snd o fst);
       
   156       val _ = List.app (Position.report pos) markup;
       
   157     in true end;
   148 
   158 
   149 fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
   159 fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
   150 
   160 
   151 fun check_tool (name, pos) =
   161 fun check_tool (name, pos) =
   152   let
   162   let
   197 
   207 
   198 in
   208 in
   199 
   209 
   200 val entity_setup =
   210 val entity_setup =
   201   entity_antiqs no_check "" "syntax" #>
   211   entity_antiqs no_check "" "syntax" #>
   202   entity_antiqs (K (is_some o Keyword.command_keyword o #1)) "isacommand" "command" #>
   212   entity_antiqs (K command_check) "isacommand" "command" #>
   203   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
   213   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
   204   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
   214   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
   205   entity_antiqs (thy_check Method.check) "" "method" #>
   215   entity_antiqs (thy_check Method.check) "" "method" #>
   206   entity_antiqs (thy_check Attrib.check) "" "attribute" #>
   216   entity_antiqs (thy_check Attrib.check) "" "attribute" #>
   207   entity_antiqs no_check "" "fact" #>
   217   entity_antiqs no_check "" "fact" #>