equal
deleted
inserted
replaced
78 val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2)); |
78 val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2)); |
79 in |
79 in |
80 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
80 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
81 ((if ! O.source then str_of_source src else txt') |
81 ((if ! O.source then str_of_source src else txt') |
82 |> (if ! O.quotes then quote else I) |
82 |> (if ! O.quotes then quote else I) |
83 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
83 |> (if ! O.display then enclose "\\begin{alltt}\\isastyleminor\n" "\n\\end{alltt}" |
84 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
84 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
85 end; |
85 end; |
86 |
86 |
87 fun output_ml ctxt src = |
87 fun output_ml ctxt src = |
88 if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
88 if ! O.display then enclose "\\begin{alltt}\\isastyleminor\n" "\n\\end{alltt}" |
89 else |
89 else |
90 split_lines |
90 split_lines |
91 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
91 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
92 #> space_implode "\\isasep\\isanewline%\n"; |
92 #> space_implode "\\isasep\\isanewline%\n"; |
93 |
93 |