# HG changeset patch
# User haftmann
# Date 1206727959 -3600
# Node ID da989545e59c6f0f883f69364a31d88803e41d9f
# Parent  21504de311979d1606add5b06921e7d73506b880
some styling

diff -r 21504de31197 -r da989545e59c doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Fri Mar 28 18:56:43 2008 +0100
+++ b/doc-src/antiquote_setup.ML	Fri Mar 28 19:12:39 2008 +0100
@@ -46,6 +46,13 @@
     else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
   end;
 
+fun output_ml ctxt src =
+  if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+    else
+    split_lines
+    #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
+    #> space_implode "\\isasep\\isanewline%\n";
+
 fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n";
 
 fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
@@ -92,6 +99,7 @@
   ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))),
   ("named_thms", O.args (Scan.repeat (Attrib.thm --
        Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")")))
-     (output_named_list pretty_thm))];
+     (output_named_list pretty_thm)),
+  ("ML_text", O.args (Scan.lift Args.name) output_ml)];
 
 end;