1.1 --- a/src/Doc/antiquote_setup.ML Wed Mar 12 12:18:41 2014 +0100
1.2 +++ b/src/Doc/antiquote_setup.ML Wed Mar 12 14:17:13 2014 +0100
1.3 @@ -4,12 +4,7 @@
1.4 Auxiliary antiquotations for the Isabelle manuals.
1.5 *)
1.6
1.7 -signature ANTIQUOTE_SETUP =
1.8 -sig
1.9 - val setup: theory -> theory
1.10 -end;
1.11 -
1.12 -structure Antiquote_Setup: ANTIQUOTE_SETUP =
1.13 +structure Antiquote_Setup: sig end =
1.14 struct
1.15
1.16 (* misc utils *)
1.17 @@ -42,9 +37,9 @@
1.18
1.19 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
1.20
1.21 -val verbatim_setup =
1.22 - Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
1.23 - (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
1.24 +val _ =
1.25 + Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
1.26 + (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")));
1.27
1.28
1.29 (* ML text *)
1.30 @@ -117,21 +112,22 @@
1.31
1.32 in
1.33
1.34 -val index_ml_setup =
1.35 - index_ml @{binding index_ML} "" ml_val #>
1.36 - index_ml @{binding index_ML_op} "infix" ml_op #>
1.37 - index_ml @{binding index_ML_type} "type" ml_type #>
1.38 - index_ml @{binding index_ML_exception} "exception" ml_exception #>
1.39 - index_ml @{binding index_ML_structure} "structure" ml_structure #>
1.40 - index_ml @{binding index_ML_functor} "functor" ml_functor;
1.41 +val _ =
1.42 + Theory.setup
1.43 + (index_ml @{binding index_ML} "" ml_val #>
1.44 + index_ml @{binding index_ML_op} "infix" ml_op #>
1.45 + index_ml @{binding index_ML_type} "type" ml_type #>
1.46 + index_ml @{binding index_ML_exception} "exception" ml_exception #>
1.47 + index_ml @{binding index_ML_structure} "structure" ml_structure #>
1.48 + index_ml @{binding index_ML_functor} "functor" ml_functor);
1.49
1.50 end;
1.51
1.52
1.53 (* named theorems *)
1.54
1.55 -val named_thms_setup =
1.56 - Thy_Output.antiquotation @{binding named_thms}
1.57 +val _ =
1.58 + Theory.setup (Thy_Output.antiquotation @{binding named_thms}
1.59 (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
1.60 (fn {context = ctxt, ...} =>
1.61 map (apfst (Thy_Output.pretty_thm ctxt))
1.62 @@ -148,15 +144,47 @@
1.63 Output.output (Pretty.str_of p) ^
1.64 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
1.65 #> space_implode "\\par\\smallskip%\n"
1.66 - #> enclose "\\isa{" "}"));
1.67 + #> enclose "\\isa{" "}")));
1.68
1.69
1.70 (* theory file *)
1.71
1.72 -val thy_file_setup =
1.73 - Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
1.74 +val _ =
1.75 + Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
1.76 (fn {context = ctxt, ...} =>
1.77 - fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
1.78 + fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
1.79 +
1.80 +
1.81 +(* Isabelle/jEdit elements *)
1.82 +
1.83 +local
1.84 +
1.85 +fun parse_named a (XML.Elem ((b, props), _)) =
1.86 + (case Properties.get props "NAME" of
1.87 + SOME name => if a = b then [name] else []
1.88 + | NONE => [])
1.89 + | parse_named _ _ = [];
1.90 +
1.91 +fun parse_dockables [XML.Elem (("DOCKABLES", _), body)] = maps (parse_named "DOCKABLE") body
1.92 + | parse_dockables _ = [];
1.93 +
1.94 +val jedit_actions =
1.95 + (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
1.96 + XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
1.97 + | _ => []);
1.98 +
1.99 +val jedit_dockables =
1.100 + (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
1.101 + XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
1.102 + | _ => []);
1.103 +
1.104 +val all_actions = jedit_actions @ jedit_dockables;
1.105 +
1.106 +in
1.107 +
1.108 +fun is_action (name, pos) = member (op =) all_actions name;
1.109 +
1.110 +end;
1.111
1.112
1.113 (* Isabelle/Isar entities (with index) *)
1.114 @@ -224,35 +252,27 @@
1.115
1.116 in
1.117
1.118 -val entity_setup =
1.119 - entity_antiqs no_check "" "syntax" #>
1.120 - entity_antiqs (K command_check) "isacommand" "command" #>
1.121 - entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
1.122 - entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
1.123 - entity_antiqs (can o Method.check_name) "" "method" #>
1.124 - entity_antiqs (can o Attrib.check_name) "" "attribute" #>
1.125 - entity_antiqs no_check "" "fact" #>
1.126 - entity_antiqs no_check "" "variable" #>
1.127 - entity_antiqs no_check "" "case" #>
1.128 - entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
1.129 - entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
1.130 - entity_antiqs no_check "isatt" "setting" #>
1.131 - entity_antiqs no_check "isatt" "system option" #>
1.132 - entity_antiqs no_check "" "inference" #>
1.133 - entity_antiqs no_check "isatt" "executable" #>
1.134 - entity_antiqs (K check_tool) "isatool" "tool" #>
1.135 - entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN;
1.136 +val _ =
1.137 + Theory.setup
1.138 + (entity_antiqs no_check "" "syntax" #>
1.139 + entity_antiqs (K command_check) "isacommand" "command" #>
1.140 + entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
1.141 + entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
1.142 + entity_antiqs (can o Method.check_name) "" "method" #>
1.143 + entity_antiqs (can o Attrib.check_name) "" "attribute" #>
1.144 + entity_antiqs no_check "" "fact" #>
1.145 + entity_antiqs no_check "" "variable" #>
1.146 + entity_antiqs no_check "" "case" #>
1.147 + entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
1.148 + entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
1.149 + entity_antiqs no_check "isatt" "setting" #>
1.150 + entity_antiqs no_check "isatt" "system option" #>
1.151 + entity_antiqs no_check "" "inference" #>
1.152 + entity_antiqs no_check "isatt" "executable" #>
1.153 + entity_antiqs (K check_tool) "isatool" "tool" #>
1.154 + entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN #>
1.155 + entity_antiqs (K is_action) "isatt" "action");
1.156
1.157 end;
1.158
1.159 -
1.160 -(* theory setup *)
1.161 -
1.162 -val setup =
1.163 - verbatim_setup #>
1.164 - index_ml_setup #>
1.165 - named_thms_setup #>
1.166 - thy_file_setup #>
1.167 - entity_setup;
1.168 -
1.169 end;