--- a/src/Doc/antiquote_setup.ML Mon Oct 20 14:11:14 2014 +0200
+++ b/src/Doc/antiquote_setup.ML Mon Oct 20 16:52:36 2014 +0200
@@ -33,15 +33,6 @@
| clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
-(* verbatim text *)
-
-val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-
-val _ =
- Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
- (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")));
-
-
(* ML text *)
local
@@ -106,11 +97,7 @@
val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
- (txt'
- |> (if Config.get ctxt Thy_Output.quotes then quote else I)
- |> (if Config.get ctxt Thy_Output.display
- then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
- else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
+ (Thy_Output.verbatim_text ctxt txt')
end);
in
@@ -281,13 +268,13 @@
entity_antiqs no_check "" @{binding case} #>
entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
- entity_antiqs no_check "isatt" @{binding setting} #>
- entity_antiqs check_system_option "isatt" @{binding system_option} #>
+ entity_antiqs no_check "isasystem" @{binding setting} #>
+ entity_antiqs check_system_option "isasystem" @{binding system_option} #>
entity_antiqs no_check "" @{binding inference} #>
- entity_antiqs no_check "isatt" @{binding executable} #>
+ entity_antiqs no_check "isasystem" @{binding executable} #>
entity_antiqs check_tool "isatool" @{binding tool} #>
entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
- entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
+ entity_antiqs (K (is_action o #1)) "isasystem" @{binding action});
end;