doc-src/antiquote_setup.ML
changeset 28759 8358fabeea95
parent 28644 e2ae4a6cf166
child 29726 5f91ff5c03a2
child 30240 5b25fee0362c
equal deleted inserted replaced
28758:4ce896a30f88 28759:8358fabeea95
    66     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    66     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    67     val _ = writeln (ml (txt1, txt2));
    67     val _ = writeln (ml (txt1, txt2));
    68     val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    68     val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    69   in
    69   in
    70     "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    70     "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    71     ((if ! O.source then ThyOutput.str_of_source src else txt')
    71     (txt'
    72     |> (if ! O.quotes then quote else I)
    72     |> (if ! O.quotes then quote else I)
    73     |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    73     |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    74         else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    74         else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    75   end;
    75   end;
    76 
    76