equal
deleted
inserted
replaced
31 | clean_name "{" = "braceleft" |
31 | clean_name "{" = "braceleft" |
32 | clean_name "}" = "braceright" |
32 | clean_name "}" = "braceright" |
33 | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c); |
33 | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c); |
34 |
34 |
35 |
35 |
36 (* verbatim text *) |
|
37 |
|
38 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
|
39 |
|
40 val _ = |
|
41 Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name) |
|
42 (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))); |
|
43 |
|
44 |
|
45 (* ML text *) |
36 (* ML text *) |
46 |
37 |
47 local |
38 local |
48 |
39 |
49 val ml_toks = ML_Lex.read Position.none; |
40 val ml_toks = ML_Lex.read Position.none; |
104 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) |
95 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) |
105 handle ERROR msg => error (msg ^ Position.here pos); |
96 handle ERROR msg => error (msg ^ Position.here pos); |
106 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
97 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
107 in |
98 in |
108 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
99 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
109 (txt' |
100 (Thy_Output.verbatim_text ctxt txt') |
110 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
|
111 |> (if Config.get ctxt Thy_Output.display |
|
112 then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
113 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
|
114 end); |
101 end); |
115 |
102 |
116 in |
103 in |
117 |
104 |
118 val _ = |
105 val _ = |
279 entity_antiqs no_check "" @{binding fact} #> |
266 entity_antiqs no_check "" @{binding fact} #> |
280 entity_antiqs no_check "" @{binding variable} #> |
267 entity_antiqs no_check "" @{binding variable} #> |
281 entity_antiqs no_check "" @{binding case} #> |
268 entity_antiqs no_check "" @{binding case} #> |
282 entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #> |
269 entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #> |
283 entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #> |
270 entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #> |
284 entity_antiqs no_check "isatt" @{binding setting} #> |
271 entity_antiqs no_check "isasystem" @{binding setting} #> |
285 entity_antiqs check_system_option "isatt" @{binding system_option} #> |
272 entity_antiqs check_system_option "isasystem" @{binding system_option} #> |
286 entity_antiqs no_check "" @{binding inference} #> |
273 entity_antiqs no_check "" @{binding inference} #> |
287 entity_antiqs no_check "isatt" @{binding executable} #> |
274 entity_antiqs no_check "isasystem" @{binding executable} #> |
288 entity_antiqs check_tool "isatool" @{binding tool} #> |
275 entity_antiqs check_tool "isatool" @{binding tool} #> |
289 entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #> |
276 entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #> |
290 entity_antiqs (K (is_action o #1)) "isatt" @{binding action}); |
277 entity_antiqs (K (is_action o #1)) "isasystem" @{binding action}); |
291 |
278 |
292 end; |
279 end; |
293 |
280 |
294 end; |
281 end; |