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;