# HG changeset patch
# User wenzelm
# Date 1516894220 -3600
# Node ID 189ab2c3026b9dfd15a8442d1f283be231dfeef1
# Parent  5db077cfe1b2eb6bd3f20063a447834fb1da4698
verbatim output consists of plain lines;

diff -r 5db077cfe1b2 -r 189ab2c3026b src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Jan 25 16:01:02 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Jan 25 16:30:20 2018 +0100
@@ -15,6 +15,7 @@
     Token.T list -> Latex.text list
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
+  val lines: Latex.text list -> Latex.text list
   val items: Latex.text list -> Latex.text list
   val isabelle: Proof.context -> Latex.text list -> Latex.text
   val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
@@ -446,6 +447,7 @@
 
 (* default output *)
 
+val lines = separate (Latex.string "\\isanewline%\n");
 val items = separate (Latex.string "\\isasep\\isanewline%\n");
 
 fun isabelle ctxt body =
@@ -464,7 +466,7 @@
 fun verbatim ctxt =
   if Config.get ctxt Document_Antiquotation.thy_output_display
   then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
-  else split_lines #> map (typewriter ctxt) #> items #> Latex.block;
+  else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
 
 fun source ctxt =
   Token.args_of_src