clarified verbatim line breaks, e.g. relevant for Implementation mldecls;

--- a/src/Pure/PIDE/resources.ML	Mon Oct 20 23:17:28 2014 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Oct 21 09:50:22 2014 +0200
@@ -224,7 +224,7 @@
     space_explode "/" name
     |> map Latex.output_ascii
     |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
-    |> Thy_Output.enclose_isabelle_tt ctxt
+    |> enclose "\\isatt{" "}"
   end;
 
 in

--- a/src/Pure/Thy/thy_output.ML	Mon Oct 20 23:17:28 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Oct 21 09:50:22 2014 +0200
@@ -35,7 +35,6 @@
     Token.src -> 'a list -> Pretty.T list
   val output: Proof.context -> Pretty.T list -> string
   val verbatim_text: Proof.context -> string -> string
-  val enclose_isabelle_tt: Proof.context -> string -> string
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -470,10 +469,6 @@
 fun tweak_line ctxt s =
   if Config.get ctxt display then s else Symbol.strip_blanks s;
 
-fun tweak_lines ctxt s =
-  if Config.get ctxt display then s
-  else s |> split_lines |> map Symbol.strip_blanks |> space_implode " ";
-
 fun pretty_text ctxt =
   Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
 
@@ -643,18 +638,18 @@
 
 (* verbatim text *)
 
-fun enclose_isabelle_tt ctxt =
-  if Config.get ctxt display
-  then enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
-  else enclose "\\isatt{" "}";
+fun verbatim_text ctxt =
+  if Config.get ctxt display then
+    Latex.output_ascii #>
+    enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
+  else
+    split_lines #>
+    map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
+    space_implode "\\isasep\\isanewline%\n";
 
-fun verbatim_text ctxt =
-  tweak_lines ctxt
-  #> Latex.output_ascii
-  #> enclose_isabelle_tt ctxt;
-
-val _ = Theory.setup
-  (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context));
+val _ =
+  Theory.setup
+    (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context));
 
 
 (* ML text *)