# HG changeset patch
# User wenzelm
# Date 1183803376 -7200
# Node ID 41cdbfb9f77b8b9796b7700be7f48b8eb86a9413
# Parent  f543538866a2ec970b24788064a69de718aef208
markup: emit as control information -- no indent text;

diff -r f543538866a2 -r 41cdbfb9f77b src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Jul 07 12:16:15 2007 +0200
+++ b/src/Pure/General/pretty.ML	Sat Jul 07 12:16:16 2007 +0200
@@ -130,6 +130,12 @@
   pos = 0,
   nl = nl + 1};
 
+fun control s {tx, ind, pos: int, nl} : text =
+ {tx = Buffer.add s tx,
+  ind = ind,
+  pos = pos,
+  nl = nl};
+
 fun string (s, len) {tx, ind, pos: int, nl} : text =
  {tx = Buffer.add s tx,
   ind = Buffer.add s ind,
@@ -192,9 +198,9 @@
               else (set_indent pos'', pos'');
             val (bg, en) = if markup = Markup.none then ("", "") else mode_markup markup;
             val btext: text = text
-              |> string (bg, 0)
+              |> control bg
               |> format (bes, block', breakdist (es, after))
-              |> string (en, 0);
+              |> control en;
             (*if this block was broken then force the next break*)
             val es' = if nl < #nl btext then forcenext es else es;
           in format (es', block, after) btext end