1.1 --- a/src/Pure/General/pretty.ML	Mon Mar 23 11:20:46 2009 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Mon Mar 23 15:23:06 2009 +0100
     1.3 @@ -104,9 +104,9 @@
     1.4  (** printing items: compound phrases, strings, and breaks **)
     1.5  
     1.6  datatype T =
     1.7 -  Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)
     1.8 -  String of output * int |                  (*text, length*)
     1.9 -  Break of bool * int;                      (*mandatory flag, width if not taken*)
    1.10 +  Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
    1.11 +  String of output * int |                           (*text, length*)
    1.12 +  Break of bool * int;                               (*mandatory flag, width if not taken*)
    1.13  
    1.14  fun length (Block (_, _, _, len)) = len
    1.15    | length (String (_, len)) = len
    1.16 @@ -124,12 +124,14 @@
    1.17  fun breaks prts = Library.separate (brk 1) prts;
    1.18  fun fbreaks prts = Library.separate fbrk prts;
    1.19  
    1.20 -fun markup_block m (indent, es) =
    1.21 +fun block_markup m (indent, es) =
    1.22    let
    1.23      fun sum [] k = k
    1.24        | sum (e :: es) k = sum es (length e + k);
    1.25    in Block (m, es, indent, sum es 0) end;
    1.26  
    1.27 +fun markup_block m arg = block_markup (Markup.output m) arg;
    1.28 +
    1.29  val blk = markup_block Markup.none;
    1.30  fun block prts = blk (2, prts);
    1.31  val strs = block o breaks o map str;
    1.32 @@ -197,7 +199,7 @@
    1.33  local
    1.34    fun pruning dp (Block (m, bes, indent, wd)) =
    1.35          if dp > 0
    1.36 -        then markup_block m (indent, map (pruning (dp - 1)) bes)
    1.37 +        then block_markup m (indent, map (pruning (dp - 1)) bes)
    1.38          else str "..."
    1.39      | pruning dp e = e
    1.40  in
    1.41 @@ -263,7 +265,7 @@
    1.42  fun format ([], _, _) text = text
    1.43    | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
    1.44        (case e of
    1.45 -        Block (markup, bes, indent, wd) =>
    1.46 +        Block ((bg, en), bes, indent, wd) =>
    1.47            let
    1.48              val {emergencypos, ...} = ! margin_info;
    1.49              val pos' = pos + indent;
    1.50 @@ -271,7 +273,6 @@
    1.51              val block' =
    1.52                if pos' < emergencypos then (ind |> add_indent indent, pos')
    1.53                else (add_indent pos'' Buffer.empty, pos'');
    1.54 -            val (bg, en) = Markup.output markup;
    1.55              val btext: text = text
    1.56                |> control bg
    1.57                |> format (bes, block', breakdist (es, after))
    1.58 @@ -303,9 +304,9 @@
    1.59  (*symbolic markup -- no formatting*)
    1.60  fun symbolic prt =
    1.61    let
    1.62 -    fun out (Block (m, [], _, _)) = Buffer.markup m I
    1.63 -      | out (Block (m, prts, indent, _)) =
    1.64 -          Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts))
    1.65 +    fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
    1.66 +      | out (Block ((bg, en), prts, indent, _)) =
    1.67 +          Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
    1.68        | out (String (s, _)) = Buffer.add s
    1.69        | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
    1.70        | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
    1.71 @@ -314,7 +315,7 @@
    1.72  (*unformatted output*)
    1.73  fun unformatted prt =
    1.74    let
    1.75 -    fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts)
    1.76 +    fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
    1.77        | fmt (String (s, _)) = Buffer.add s
    1.78        | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
    1.79        | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
    1.80 @@ -323,11 +324,11 @@
    1.81  
    1.82  (* ML toplevel pretty printing *)
    1.83  
    1.84 -fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
    1.85 +fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
    1.86    | to_ML (String s) = ML_Pretty.String s
    1.87    | to_ML (Break b) = ML_Pretty.Break b;
    1.88  
    1.89 -fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
    1.90 +fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
    1.91    | from_ML (ML_Pretty.String s) = String s
    1.92    | from_ML (ML_Pretty.Break b) = Break b;
    1.93