1(* Title: Doc/antiquote_setup.ML 2 Author: Makarius 3 4Auxiliary antiquotations for the Isabelle manuals. 5*) 6 7structure Antiquote_Setup: sig end = 8struct 9 10(* misc utils *) 11 12fun translate f = Symbol.explode #> map f #> implode; 13 14val clean_string = translate 15 (fn "_" => "\\_" 16 | "#" => "\\#" 17 | "$" => "\\$" 18 | "%" => "\\%" 19 | "<" => "$<$" 20 | ">" => "$>$" 21 | "{" => "\\{" 22 | "|" => "$\\mid$" 23 | "}" => "\\}" 24 | "\<hyphen>" => "-" 25 | c => c); 26 27fun clean_name "\<dots>" = "dots" 28 | clean_name ".." = "ddot" 29 | clean_name "." = "dot" 30 | clean_name "_" = "underscore" 31 | clean_name "{" = "braceleft" 32 | clean_name "}" = "braceright" 33 | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c); 34 35 36(* ML text *) 37 38local 39 40fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");" 41 | ml_val (toks1, toks2) = 42 ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; 43 44fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");" 45 | ml_op (toks1, toks2) = 46 ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; 47 48fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;" 49 | ml_type (toks1, toks2) = 50 ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @ 51 toks2 @ ML_Lex.read ") option];"; 52 53fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);" 54 | ml_exception (toks1, toks2) = 55 ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);"; 56 57fun ml_structure (toks, _) = 58 ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;"; 59 60fun ml_functor (Antiquote.Text tok :: _, _) = 61 ML_Lex.read "ML_Env.check_functor " @ 62 ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok)) 63 | ml_functor _ = raise Fail "Bad ML functor specification"; 64 65val is_name = 66 ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident); 67 68fun ml_name txt = 69 (case filter is_name (ML_Lex.tokenize txt) of 70 toks as [_] => ML_Lex.flatten toks 71 | _ => error ("Single ML name expected in input: " ^ quote txt)); 72 73fun prep_ml source = 74 (#1 (Input.source_content source), ML_Lex.read_source source); 75 76fun index_ml name kind ml = Thy_Output.antiquotation_raw name 77 (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input))) 78 (fn ctxt => fn (source1, opt_source2) => 79 let 80 val (txt1, toks1) = prep_ml source1; 81 val (txt2, toks2) = 82 (case opt_source2 of 83 SOME source => prep_ml source 84 | NONE => ("", [])); 85 86 val txt = 87 if txt2 = "" then txt1 88 else if kind = "type" then txt1 ^ " = " ^ txt2 89 else if kind = "exception" then txt1 ^ " of " ^ txt2 90 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) 91 then txt1 ^ ": " ^ txt2 92 else txt1 ^ " : " ^ txt2; 93 val txt' = if kind = "" then txt else kind ^ " " ^ txt; 94 95 val pos = Input.pos_of source1; 96 val _ = 97 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) 98 handle ERROR msg => error (msg ^ Position.here pos); 99 val kind' = if kind = "" then "ML" else "ML " ^ kind; 100 in 101 Latex.block 102 [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"), 103 Thy_Output.verbatim ctxt txt'] 104 end); 105 106in 107 108val _ = 109 Theory.setup 110 (index_ml \<^binding>\<open>index_ML\<close> "" ml_val #> 111 index_ml \<^binding>\<open>index_ML_op\<close> "infix" ml_op #> 112 index_ml \<^binding>\<open>index_ML_type\<close> "type" ml_type #> 113 index_ml \<^binding>\<open>index_ML_exception\<close> "exception" ml_exception #> 114 index_ml \<^binding>\<open>index_ML_structure\<close> "structure" ml_structure #> 115 index_ml \<^binding>\<open>index_ML_functor\<close> "functor" ml_functor); 116 117end; 118 119 120(* named theorems *) 121 122val _ = 123 Theory.setup (Thy_Output.antiquotation_raw \<^binding>\<open>named_thms\<close> 124 (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) 125 (fn ctxt => 126 map (fn (thm, name) => 127 Output.output 128 (Document_Antiquotation.format ctxt 129 (Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^ 130 enclose "\\rulename{" "}" (Output.output name)) 131 #> space_implode "\\par\\smallskip%\n" 132 #> Latex.string #> single 133 #> Thy_Output.isabelle ctxt)); 134 135 136(* Isabelle/Isar entities (with index) *) 137 138local 139 140fun no_check (_: Proof.context) (name, _: Position.T) = name; 141 142fun check_keyword ctxt (name, pos) = 143 if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name 144 else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos); 145 146fun check_system_option ctxt (name, pos) = 147 (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true) 148 handle ERROR _ => false; 149 150val arg = enclose "{" "}" o clean_string; 151 152fun entity check markup binding index = 153 Thy_Output.antiquotation_raw 154 (binding |> Binding.map_name (fn name => name ^ 155 (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) 156 (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name_position)) 157 (fn ctxt => fn (logic, (name, pos)) => 158 let 159 val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); 160 val hyper_name = 161 "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; 162 val hyper = 163 enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> 164 index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; 165 val idx = 166 (case index of 167 NONE => "" 168 | SOME is_def => 169 "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); 170 val _ = 171 if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else (); 172 val latex = 173 idx ^ 174 (Output.output name 175 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") 176 |> hyper o enclose "\\mbox{\\isa{" "}}"); 177 in Latex.string latex end); 178 179fun entity_antiqs check markup kind = 180 entity check markup kind NONE #> 181 entity check markup kind (SOME true) #> 182 entity check markup kind (SOME false); 183 184in 185 186val _ = 187 Theory.setup 188 (entity_antiqs no_check "" \<^binding>\<open>syntax\<close> #> 189 entity_antiqs Outer_Syntax.check_command "isacommand" \<^binding>\<open>command\<close> #> 190 entity_antiqs check_keyword "isakeyword" \<^binding>\<open>keyword\<close> #> 191 entity_antiqs check_keyword "isakeyword" \<^binding>\<open>element\<close> #> 192 entity_antiqs Method.check_name "" \<^binding>\<open>method\<close> #> 193 entity_antiqs Attrib.check_name "" \<^binding>\<open>attribute\<close> #> 194 entity_antiqs no_check "" \<^binding>\<open>fact\<close> #> 195 entity_antiqs no_check "" \<^binding>\<open>variable\<close> #> 196 entity_antiqs no_check "" \<^binding>\<open>case\<close> #> 197 entity_antiqs Document_Antiquotation.check "" \<^binding>\<open>antiquotation\<close> #> 198 entity_antiqs Document_Antiquotation.check_option "" \<^binding>\<open>antiquotation_option\<close> #> 199 entity_antiqs Document_Marker.check "" \<^binding>\<open>document_marker\<close> #> 200 entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #> 201 entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #> 202 entity_antiqs no_check "" \<^binding>\<open>inference\<close> #> 203 entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #> 204 entity_antiqs no_check "isatool" \<^binding>\<open>tool\<close> #> 205 entity_antiqs ML_Context.check_antiquotation "" \<^binding>\<open>ML_antiquotation\<close> #> 206 entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close>); 207 208end; 209 210end; 211