doc-src/antiquote_setup.ML
changeset 43564 9864182c6bad
parent 43563 aeabb735883a
child 45675 ac54a3abff81
     1.1 --- a/doc-src/antiquote_setup.ML	Mon Jun 27 17:51:28 2011 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Jun 27 22:20:49 2011 +0200
     1.3 @@ -4,7 +4,12 @@
     1.4  Auxiliary antiquotations for the Isabelle manuals.
     1.5  *)
     1.6  
     1.7 -structure Antiquote_Setup: sig end =
     1.8 +signature ANTIQUOTE_SETUP =
     1.9 +sig
    1.10 +  val setup: theory -> theory
    1.11 +end;
    1.12 +
    1.13 +structure Antiquote_Setup: ANTIQUOTE_SETUP =
    1.14  struct
    1.15  
    1.16  (* misc utils *)
    1.17 @@ -35,8 +40,9 @@
    1.18  
    1.19  val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    1.20  
    1.21 -val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name)
    1.22 -  (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
    1.23 +val verbatim_setup =
    1.24 +  Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
    1.25 +    (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
    1.26  
    1.27  
    1.28  (* ML text *)
    1.29 @@ -87,42 +93,45 @@
    1.30  
    1.31  in
    1.32  
    1.33 -val _ = index_ml "index_ML" "" ml_val;
    1.34 -val _ = index_ml "index_ML_type" "type" ml_type;
    1.35 -val _ = index_ml "index_ML_exn" "exception" ml_exn;
    1.36 -val _ = index_ml "index_ML_structure" "structure" ml_structure;
    1.37 -val _ = index_ml "index_ML_functor" "functor" ml_functor;
    1.38 +val index_ml_setup =
    1.39 +  index_ml @{binding index_ML} "" ml_val #>
    1.40 +  index_ml @{binding index_ML_type} "type" ml_type #>
    1.41 +  index_ml @{binding index_ML_exn} "exception" ml_exn #>
    1.42 +  index_ml @{binding index_ML_structure} "structure" ml_structure #>
    1.43 +  index_ml @{binding index_ML_functor} "functor" ml_functor;
    1.44  
    1.45  end;
    1.46  
    1.47  
    1.48  (* named theorems *)
    1.49  
    1.50 -val _ = Thy_Output.antiquotation "named_thms"
    1.51 -  (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
    1.52 -  (fn {context = ctxt, ...} =>
    1.53 -    map (apfst (Thy_Output.pretty_thm ctxt))
    1.54 -    #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
    1.55 -    #> (if Config.get ctxt Thy_Output.display
    1.56 -        then
    1.57 -          map (fn (p, name) =>
    1.58 -            Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
    1.59 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.60 -          #> space_implode "\\par\\smallskip%\n"
    1.61 -          #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.62 -        else
    1.63 -          map (fn (p, name) =>
    1.64 -            Output.output (Pretty.str_of p) ^
    1.65 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.66 -          #> space_implode "\\par\\smallskip%\n"
    1.67 -          #> enclose "\\isa{" "}"));
    1.68 +val named_thms_setup =
    1.69 +  Thy_Output.antiquotation @{binding named_thms}
    1.70 +    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
    1.71 +    (fn {context = ctxt, ...} =>
    1.72 +      map (apfst (Thy_Output.pretty_thm ctxt))
    1.73 +      #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
    1.74 +      #> (if Config.get ctxt Thy_Output.display
    1.75 +          then
    1.76 +            map (fn (p, name) =>
    1.77 +              Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
    1.78 +              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.79 +            #> space_implode "\\par\\smallskip%\n"
    1.80 +            #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.81 +          else
    1.82 +            map (fn (p, name) =>
    1.83 +              Output.output (Pretty.str_of p) ^
    1.84 +              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.85 +            #> space_implode "\\par\\smallskip%\n"
    1.86 +            #> enclose "\\isa{" "}"));
    1.87  
    1.88  
    1.89  (* theory file *)
    1.90  
    1.91 -val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
    1.92 -  (fn {context = ctxt, ...} =>
    1.93 -    fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
    1.94 +val thy_file_setup =
    1.95 +  Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
    1.96 +    (fn {context = ctxt, ...} =>
    1.97 +      fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
    1.98  
    1.99  
   1.100  (* Isabelle/Isar entities (with index) *)
   1.101 @@ -142,8 +151,8 @@
   1.102  
   1.103  fun entity check markup kind index =
   1.104    Thy_Output.antiquotation
   1.105 -    (translate (fn " " => "_" | c => c) kind ^
   1.106 -      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
   1.107 +    (Binding.name (translate (fn " " => "_" | c => c) kind ^
   1.108 +      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
   1.109      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
   1.110      (fn {context = ctxt, ...} => fn (logic, name) =>
   1.111        let
   1.112 @@ -170,32 +179,44 @@
   1.113        end);
   1.114  
   1.115  fun entity_antiqs check markup kind =
   1.116 - ((entity check markup kind NONE);
   1.117 -  (entity check markup kind (SOME true));
   1.118 -  (entity check markup kind (SOME false)));
   1.119 +  entity check markup kind NONE #>
   1.120 +  entity check markup kind (SOME true) #>
   1.121 +  entity check markup kind (SOME false);
   1.122  
   1.123  in
   1.124  
   1.125 -val _ = entity_antiqs no_check "" "syntax";
   1.126 -val _ = entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command";
   1.127 -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword";
   1.128 -val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "element";
   1.129 -val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
   1.130 -val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
   1.131 -val _ = entity_antiqs no_check "" "fact";
   1.132 -val _ = entity_antiqs no_check "" "variable";
   1.133 -val _ = entity_antiqs no_check "" "case";
   1.134 -val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation";
   1.135 -val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option";
   1.136 -val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
   1.137 -val _ = entity_antiqs no_check "" "inference";
   1.138 -val _ = entity_antiqs no_check "isatt" "executable";
   1.139 -val _ = entity_antiqs (K check_tool) "isatt" "tool";
   1.140 -val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
   1.141 -val _ =
   1.142 -  entity_antiqs
   1.143 -    (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) "" Markup.ML_antiquotationN;
   1.144 +val entity_setup =
   1.145 +  entity_antiqs no_check "" "syntax" #>
   1.146 +  entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command" #>
   1.147 +  entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword" #>
   1.148 +  entity_antiqs (K Keyword.is_keyword) "isakeyword" "element" #>
   1.149 +  entity_antiqs (thy_check Method.intern Method.defined) "" "method" #>
   1.150 +  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" #>
   1.151 +  entity_antiqs no_check "" "fact" #>
   1.152 +  entity_antiqs no_check "" "variable" #>
   1.153 +  entity_antiqs no_check "" "case" #>
   1.154 +  entity_antiqs (thy_check Thy_Output.intern_command Thy_Output.defined_command)
   1.155 +    "" "antiquotation" #>
   1.156 +  entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option)
   1.157 +    "" "antiquotation option" #>
   1.158 +  entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" #>
   1.159 +  entity_antiqs no_check "" "inference" #>
   1.160 +  entity_antiqs no_check "isatt" "executable" #>
   1.161 +  entity_antiqs (K check_tool) "isatt" "tool" #>
   1.162 +  entity_antiqs (K (can Thy_Info.get_theory)) "" "theory" #>
   1.163 +  entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
   1.164 +    "" Markup.ML_antiquotationN;
   1.165  
   1.166  end;
   1.167  
   1.168 +
   1.169 +(* theory setup *)
   1.170 +
   1.171 +val setup =
   1.172 +  verbatim_setup #>
   1.173 +  index_ml_setup #>
   1.174 +  named_thms_setup #>
   1.175 +  thy_file_setup #>
   1.176 +  entity_setup;
   1.177 +
   1.178  end;