src/Doc/antiquote_setup.ML
changeset 61618 27af754f50ca
parent 61617 cd7549cd5fe7
child 61620 01db1bed4487
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Nov 10 20:10:17 2015 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Nov 10 20:49:48 2015 +0100
     1.3 @@ -150,20 +150,7 @@
     1.4  fun is_keyword ctxt (name, _) =
     1.5    Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name;
     1.6  
     1.7 -fun check_command ctxt (name, pos) =
     1.8 -  let
     1.9 -    val thy = Proof_Context.theory_of ctxt;
    1.10 -    val keywords = Thy_Header.get_keywords thy;
    1.11 -  in
    1.12 -    Keyword.is_command keywords name andalso
    1.13 -      let
    1.14 -        val markup =
    1.15 -          Token.explode keywords Position.none name
    1.16 -          |> maps (Outer_Syntax.command_reports thy)
    1.17 -          |> map (snd o fst);
    1.18 -        val _ = Context_Position.reports ctxt (map (pair pos) markup);
    1.19 -      in true end
    1.20 -  end;
    1.21 +fun check_command ctxt (name, pos) = (Outer_Syntax.check_command ctxt (name, pos); true);
    1.22  
    1.23  fun check_system_option ctxt (name, pos) =
    1.24    (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)