equal
deleted
inserted
replaced
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 |