src/Pure/General/pretty.ML

 
 (* formatted output *)
 
 local
 
-type text = {markups: Markup.output list, tx: Bytes.T, ind: Buffer.T, pos: int, nl: int};
-
-val empty: text =
- {markups = [],
-  tx = Bytes.empty,
-  ind = Buffer.empty,
-  pos = 0,
-  nl = 0};
-
-fun string (s, len) {markups, tx, ind, pos: int, nl} : text =
- {markups = markups,
-  tx = Bytes.add s tx,
-  ind = Buffer.add s ind,
+type context = Markup.output list;  (*stack of pending markup*)
+
+abstype state = State of context * Bytes.T
+with
+
+fun state_output (State (_, output)) = output;
+
+val empty_state = State ([], Bytes.empty);
+
+fun add_state s (State (context, output)) =
+  State (context, Bytes.add s output);
+
+fun push_state (markup as (bg, _)) (State (context, output)) =
+  State (markup :: context, Bytes.add bg output);
+
+fun pop_state (State ((_, en) :: context, output)) =
+  State (context, Bytes.add en output);
+
+end;
+
+type text = {main: state, line: state, pos: int, nl: int};
+
+val empty: text = {main = empty_state, line = empty_state, pos = 0, nl = 0};
+
+fun string (s, len) {main, line, pos, nl} : text =
+ {main = add_state s main,
+  line = add_state s line,
   pos = pos + len,
   nl = nl};
 
-fun push (markup as (bg, _)) {markups, tx, ind, pos: int, nl} : text =
- {markups = markup :: markups,
-  tx = Bytes.add bg tx,
-  ind = ind,
+fun push m {main, line, pos, nl} : text =
+ {main = push_state m main,
+  line = line,
   pos = pos,
   nl = nl};
 
-fun pop {markups = (_, en) :: markups, tx, ind, pos: int, nl} : text =
- {markups = markups,
-  tx = Bytes.add en tx,
-  ind = ind,
+fun pop {main, line, pos, nl} : text =
+ {main = pop_state main,
+  line = line,
   pos = pos,
   nl = nl};
+
+fun result ({main, ...}: text) = state_output main;
 
 (*Add the lengths of the expressions until the next Break; if no Break then
   include "after", to account for text following this block.*)
 fun break_dist (Break _ :: _, _) = 0
   | break_dist (prt :: prts, after) = tree_length prt + break_dist (prts, after)

     val newline = output_newline ops;
     val blanks = string o output_spaces ops;
 
     val indent_markup = #indent_markup ops;
     val no_indent_markup = indent_markup = Markup.no_output;
-    val (indent_bg, indent_en) = apply2 Substring.full indent_markup;
-
-    val add_indent = if no_indent_markup then K I else output_spaces_buffer ops;
-
-    fun break_indent (buf, n) ({markups, tx, nl, ...}: text) : text =
+
+    val add_indent = if no_indent_markup then K I else add_state o #1 o output_spaces ops;
+
+    fun break_indent (before_state, before_pos) ({main, line, nl, ...}: text) : text =
       let
-        val s = Buffer.content buf;
-        val indent =
-          if no_indent_markup then Bytes.add (Symbol.spaces n)
-          else if s = "" then I
-          else Bytes.add_substring indent_bg #> Bytes.add s #> Bytes.add_substring indent_en;
-        val tx' = tx |> Bytes.add newline |> indent;
-        val ind' = Buffer.add s Buffer.empty;
-      in {markups = markups, tx = tx', ind = ind', pos = n, nl = nl + 1} end;
-
-    nonfix before;
+        val (main', line') =
+          if no_indent_markup then
+            (main |> add_state newline |> add_state (Symbol.spaces before_pos), line)
+          else
+            let
+              val ss = Bytes.contents (state_output before_state);
+              val main' = main |> add_state newline
+                |> not (null ss) ? (push_state indent_markup #> fold add_state ss #> pop_state);
+              val line' = fold add_state ss empty_state;
+            in (main', line') end;
+      in {main = main', line = line', pos = before_pos, nl = nl + 1} end;
 
     (*'before' is the indentation context of the current block*)
     (*'after' is the width of the input context until the next break*)
     fun format (trees, before, after) (text as {pos, ...}) =
       (case trees of

           let
             val pos' = pos + indent;
             val pos'' = pos' mod emergencypos;
             val before' =
               if pos' < emergencypos
-              then (add_indent indent (#ind text), pos')
-              else (add_indent pos'' Buffer.empty, pos'');
+              then (add_indent indent (#line text), pos')
+              else (add_indent pos'' empty_state, pos'');
             val after' = break_dist (ts, after)
             val body' = body
               |> (consistent andalso pos + blen > margin - after') ? map force_break;
             val btext: text =
               text |> push markup |> format (body' @ [End], before', after');

                 pos + wd <= Int.max (margin - break_dist (ts, after), #2 before + breakgain)
              then text |> blanks wd  (*just insert wd blanks*)
              else text |> break_indent before |> blanks ind)
       | Str str :: ts => format (ts, before, after) (string str text));
   in
-    #tx (format ([output_tree ops true input], (Buffer.empty, 0), 0) empty)
+    result (format ([output_tree ops true input], (empty_state, 0), 0) empty)
   end;
 
 end;