Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
to_ML/from_ML: proper handling of markup;

--- a/src/Pure/General/pretty.ML	Mon Mar 23 11:20:46 2009 +0100
+++ b/src/Pure/General/pretty.ML	Mon Mar 23 15:23:06 2009 +0100
@@ -104,9 +104,9 @@
 (** 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
@@ -124,12 +124,14 @@
 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;
@@ -197,7 +199,7 @@
 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
@@ -263,7 +265,7 @@
 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;
@@ -271,7 +273,6 @@
             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))
@@ -303,9 +304,9 @@
 (*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));
@@ -314,7 +315,7 @@
 (*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);
@@ -323,11 +324,11 @@
 
 (* 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;