src/Doc/antiquote_setup.ML
changeset 56185 851c7b05eb92
parent 56135 efa24d31e595
child 56208 06cc31dff138
     1.1 --- a/src/Doc/antiquote_setup.ML	Mon Mar 17 20:22:04 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Mon Mar 17 20:48:58 2014 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4  
     1.5  fun no_check _ _ = true;
     1.6  
     1.7 -fun command_check (name, pos) =
     1.8 +fun check_command (name, pos) =
     1.9    is_some (Keyword.command_keyword name) andalso
    1.10      let
    1.11        val markup =
    1.12 @@ -213,13 +213,14 @@
    1.13  
    1.14  val arg = enclose "{" "}" o clean_string;
    1.15  
    1.16 -fun entity check markup kind index =
    1.17 +fun entity check markup binding index =
    1.18    Thy_Output.antiquotation
    1.19 -    (Binding.name (translate (fn " " => "_" | c => c) kind ^
    1.20 +    (binding |> Binding.map_name (fn name => name ^
    1.21        (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
    1.22      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
    1.23      (fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
    1.24        let
    1.25 +        val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
    1.26          val hyper_name =
    1.27            "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
    1.28          val hyper =
    1.29 @@ -251,24 +252,24 @@
    1.30  
    1.31  val _ =
    1.32    Theory.setup
    1.33 -   (entity_antiqs no_check "" "syntax" #>
    1.34 -    entity_antiqs (K command_check) "isacommand" "command" #>
    1.35 -    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
    1.36 -    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
    1.37 -    entity_antiqs (can o Method.check_name) "" "method" #>
    1.38 -    entity_antiqs (can o Attrib.check_name) "" "attribute" #>
    1.39 -    entity_antiqs no_check "" "fact" #>
    1.40 -    entity_antiqs no_check "" "variable" #>
    1.41 -    entity_antiqs no_check "" "case" #>
    1.42 -    entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
    1.43 -    entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
    1.44 -    entity_antiqs no_check "isatt" "setting" #>
    1.45 -    entity_antiqs no_check "isatt" "system option" #>
    1.46 -    entity_antiqs no_check "" "inference" #>
    1.47 -    entity_antiqs no_check "isatt" "executable" #>
    1.48 -    entity_antiqs (K check_tool) "isatool" "tool" #>
    1.49 -    entity_antiqs (can o ML_Context.check_antiquotation) "" Markup.ML_antiquotationN #>
    1.50 -    entity_antiqs (K (is_action o #1)) "isatt" "action");
    1.51 +   (entity_antiqs no_check "" @{binding syntax} #>
    1.52 +    entity_antiqs (K check_command) "isacommand" @{binding command} #>
    1.53 +    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
    1.54 +    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
    1.55 +    entity_antiqs (can o Method.check_name) "" @{binding method} #>
    1.56 +    entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #>
    1.57 +    entity_antiqs no_check "" @{binding fact} #>
    1.58 +    entity_antiqs no_check "" @{binding variable} #>
    1.59 +    entity_antiqs no_check "" @{binding case} #>
    1.60 +    entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
    1.61 +    entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
    1.62 +    entity_antiqs no_check "isatt" @{binding setting} #>
    1.63 +    entity_antiqs no_check "isatt" @{binding system_option} #>
    1.64 +    entity_antiqs no_check "" @{binding inference} #>
    1.65 +    entity_antiqs no_check "isatt" @{binding executable} #>
    1.66 +    entity_antiqs (K check_tool) "isatool" @{binding tool} #>
    1.67 +    entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
    1.68 +    entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
    1.69  
    1.70  end;
    1.71