1.1 --- a/doc-src/antiquote_setup.ML Fri Mar 28 18:56:43 2008 +0100
1.2 +++ b/doc-src/antiquote_setup.ML Fri Mar 28 19:12:39 2008 +0100
1.3 @@ -46,6 +46,13 @@
1.4 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
1.5 end;
1.6
1.7 +fun output_ml ctxt src =
1.8 + if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.9 + else
1.10 + split_lines
1.11 + #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
1.12 + #> space_implode "\\isasep\\isanewline%\n";
1.13 +
1.14 fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n";
1.15
1.16 fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
1.17 @@ -92,6 +99,7 @@
1.18 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))),
1.19 ("named_thms", O.args (Scan.repeat (Attrib.thm --
1.20 Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")")))
1.21 - (output_named_list pretty_thm))];
1.22 + (output_named_list pretty_thm)),
1.23 + ("ML_text", O.args (Scan.lift Args.name) output_ml)];
1.24
1.25 end;