src/Doc/antiquote_setup.ML
changeset 55743 225a060e7445
parent 55742 a989bdaf8121
child 55828 42ac3cfb89f6
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Feb 25 14:34:18 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Feb 25 14:56:58 2014 +0100
     1.3 @@ -156,8 +156,6 @@
     1.4        val _ = List.app (Position.report pos) markup;
     1.5      in true end;
     1.6  
     1.7 -fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
     1.8 -
     1.9  fun check_tool (name, pos) =
    1.10    let
    1.11      fun tool dir =
    1.12 @@ -213,18 +211,18 @@
    1.13    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
    1.14    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
    1.15    entity_antiqs (can o Method.check_name) "" "method" #>
    1.16 -  entity_antiqs (thy_check Attrib.check) "" "attribute" #>
    1.17 +  entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #>
    1.18    entity_antiqs no_check "" "fact" #>
    1.19    entity_antiqs no_check "" "variable" #>
    1.20    entity_antiqs no_check "" "case" #>
    1.21 -  entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #>
    1.22 -  entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #>
    1.23 +  entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
    1.24 +  entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
    1.25    entity_antiqs no_check "isatt" "setting" #>
    1.26    entity_antiqs no_check "isatt" "system option" #>
    1.27    entity_antiqs no_check "" "inference" #>
    1.28    entity_antiqs no_check "isatt" "executable" #>
    1.29    entity_antiqs (K check_tool) "isatool" "tool" #>
    1.30 -  entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN;
    1.31 +  entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN;
    1.32  
    1.33  end;
    1.34