src/Pure/General/pretty.ML

 
 
 (** printing items: compound phrases, strings, and breaks **)
 
 datatype T =
-  Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)
-  String of output * int |                  (*text, length*)
-  Break of bool * int;                      (*mandatory flag, width if not taken*)
+  Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
+  String of output * int |                           (*text, length*)
+  Break of bool * int;                               (*mandatory flag, width if not taken*)
 
 fun length (Block (_, _, _, len)) = len
   | length (String (_, len)) = len
   | length (Break (_, wd)) = wd;
 

 val fbrk = Break (true, 2);
 
 fun breaks prts = Library.separate (brk 1) prts;
 fun fbreaks prts = Library.separate fbrk prts;
 
-fun markup_block m (indent, es) =
+fun block_markup m (indent, es) =
   let
     fun sum [] k = k
       | sum (e :: es) k = sum es (length e + k);
   in Block (m, es, indent, sum es 0) end;
 
+fun markup_block m arg = block_markup (Markup.output m) arg;
+
 val blk = markup_block Markup.none;
 fun block prts = blk (2, prts);
 val strs = block o breaks o map str;
 
 fun markup m prts = markup_block m (0, prts);

 fun setdepth dp = (depth := dp);
 
 local
   fun pruning dp (Block (m, bes, indent, wd)) =
         if dp > 0
-        then markup_block m (indent, map (pruning (dp - 1)) bes)
+        then block_markup m (indent, map (pruning (dp - 1)) bes)
         else str "..."
     | pruning dp e = e
 in
   fun prune e = if ! depth > 0 then pruning (! depth) e else e;
 end;

   blockin is the indentation of the current block;
   after is the width of the following context until next break.*)
 fun format ([], _, _) text = text
   | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
       (case e of
-        Block (markup, bes, indent, wd) =>
+        Block ((bg, en), bes, indent, wd) =>
           let
             val {emergencypos, ...} = ! margin_info;
             val pos' = pos + indent;
             val pos'' = pos' mod emergencypos;
             val block' =
               if pos' < emergencypos then (ind |> add_indent indent, pos')
               else (add_indent pos'' Buffer.empty, pos'');
-            val (bg, en) = Markup.output markup;
             val btext: text = text
               |> control bg
               |> format (bes, block', breakdist (es, after))
               |> control en;
             (*if this block was broken then force the next break*)

 (* special output *)
 
 (*symbolic markup -- no formatting*)
 fun symbolic prt =
   let
-    fun out (Block (m, [], _, _)) = Buffer.markup m I
-      | out (Block (m, prts, indent, _)) =
-          Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts))
+    fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
+      | out (Block ((bg, en), prts, indent, _)) =
+          Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
       | out (String (s, _)) = Buffer.add s
       | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
       | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
   in out prt Buffer.empty end;
 
 (*unformatted output*)
 fun unformatted prt =
   let
-    fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts)
+    fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
       | fmt (String (s, _)) = Buffer.add s
       | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
       | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
   in fmt (prune prt) Buffer.empty end;
 
 
 (* ML toplevel pretty printing *)
 
-fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
+fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
   | to_ML (String s) = ML_Pretty.String s
   | to_ML (Break b) = ML_Pretty.Break b;
 
-fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
+fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
   | from_ML (ML_Pretty.String s) = String s
   | from_ML (ML_Pretty.Break b) = Break b;
 
 
 (* output interfaces *)