src/Doc/antiquote_setup.ML
changeset 56059 2390391584c2
parent 55997 9dc5ce83202c
child 56060 61f319bebb7a
     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;