equal
deleted
inserted
replaced
599 |
599 |
600 (* verbatim text *) |
600 (* verbatim text *) |
601 |
601 |
602 fun verbatim_text ctxt = |
602 fun verbatim_text ctxt = |
603 if Config.get ctxt display then |
603 if Config.get ctxt display then |
|
604 split_lines #> map (prefix (Pretty.spaces (Config.get ctxt indent))) #> cat_lines #> |
604 Latex.output_ascii #> Latex.environment "isabellett" |
605 Latex.output_ascii #> Latex.environment "isabellett" |
605 else |
606 else |
606 split_lines #> |
607 split_lines #> |
607 map (Latex.output_ascii #> enclose "\\isatt{" "}") #> |
608 map (Latex.output_ascii #> enclose "\\isatt{" "}") #> |
608 space_implode "\\isasep\\isanewline%\n"; |
609 space_implode "\\isasep\\isanewline%\n"; |