ignore ThyOutput.source flag;
authorwenzelm
Thu, 13 Nov 2008 21:41:04 +0100
changeset 287598358fabeea95
parent 28758 4ce896a30f88
child 28760 cbc435f7b16b
ignore ThyOutput.source flag;
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Thu Nov 13 21:40:30 2008 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Thu Nov 13 21:41:04 2008 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
     1.5    in
     1.6      "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
     1.7 -    ((if ! O.source then ThyOutput.str_of_source src else txt')
     1.8 +    (txt'
     1.9      |> (if ! O.quotes then quote else I)
    1.10      |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.11          else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))