src/Pure/General/pretty.ML

   val add_mode: string -> ops -> unit
   val get_mode: unit -> ops
   type T
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
-  val make_block: {markup: Markup.output, consistent: bool, indent: int} ->
-    T list -> T
+  val make_block: {markup: Markup.output, consistent: bool, indent: int} -> T list -> T
   val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T
   val str: string -> T
   val dots: T
   val brk: int -> T
   val brk_indent: int -> int -> T

     markup: Markup.output -> Markup.output,
     indent: string -> int -> Output.output,
     margin: int}
   val output_ops: int option -> output_ops
   val markup_output_ops: int option -> output_ops
+  val symbolic_output: T -> Output.output list
+  val symbolic_string_of: T -> string
+  val unformatted_string_of: T -> string
   val regularN: string
   val symbolicN: string
   val output_buffer: output_ops -> T -> Buffer.T
   val output: output_ops -> T -> Output.output list
   val string_of_ops: output_ops -> T -> string
   val string_of: T -> string
   val writeln: T -> unit
-  val symbolic_output: T -> Output.output list
-  val symbolic_string_of: T -> string
-  val unformatted_string_of: T -> string
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
   val chunks2: T list -> T
   val block_enclose: T * T -> T list -> T
   val writeln_chunks: T list -> unit

 
 (** print mode operations **)
 
 type ops = {markup: Markup.output -> Markup.output, indent: string -> int -> string};
 
-val markup_ops : ops = {markup = I, indent = K Symbol.spaces};
-val no_markup_ops : ops = {markup = K Markup.no_output, indent = #indent markup_ops};
+val markup_ops: ops = {markup = I, indent = K Symbol.spaces};
+val no_markup_ops: ops = {markup = K Markup.no_output, indent = #indent markup_ops};
 
 local
   val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", no_markup_ops)]);
 in
   fun add_mode name ops =

       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 
 
-(** printing items: compound phrases, strings, and breaks **)
+(** Pretty.T **)
+
+(* abstype: ML_Pretty.pretty without (op =) *)
+
+abstype T = T of ML_Pretty.pretty
+with
+  fun to_ML (T prt) = prt;
+  val from_ML = T;
+end;
 
 val force_nat = Integer.max 0;
 val short_nat = FixedInt.fromInt o force_nat;
 val long_nat = force_nat o FixedInt.toInt;
 
-datatype tree =
-    Block of Markup.output * bool * int * tree list * int
-      (*markup output, consistent, indentation, body, length*)
-  | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
-  | Str of Output.output * int;  (*string output, length*)
-
-fun tree_length (Block (_, _, _, _, len)) = len
-  | tree_length (Break (_, wd, _)) = wd
-  | tree_length (Str (_, len)) = len;
-
-abstype T = T of ML_Pretty.pretty
-with
-
-fun to_ML (T prt) = prt;
-val from_ML = T;
+
+(* primitives *)
 
 fun make_block {markup = (bg, en), consistent, indent} body =
   let
     val context =
       (if bg = "" then [] else [ML_Pretty.ContextProperty ("begin", bg)]) @
       (if en = "" then [] else [ML_Pretty.ContextProperty ("end", en)]);
     val ind = short_nat indent;
-  in T (ML_Pretty.PrettyBlock (ind, consistent, context, map to_ML body)) end;
+  in from_ML (ML_Pretty.PrettyBlock (ind, consistent, context, map to_ML body)) end;
 
 fun markup_block {markup, consistent, indent} body =
   make_block {markup = YXML.output_markup markup, consistent = consistent, indent = indent} body;
 
-
-
-(** derived operations to create formatting expressions **)
-
-val str = T o ML_Pretty.str;
-val dots = T ML_Pretty.dots;
-
-fun brk_indent wd ind = T (ML_Pretty.PrettyBreak (short_nat wd, short_nat ind));
+val str = from_ML o ML_Pretty.str;
+val dots = from_ML ML_Pretty.dots;
+
+fun brk_indent wd ind = from_ML (ML_Pretty.PrettyBreak (short_nat wd, short_nat ind));
 fun brk wd = brk_indent wd 0;
-val fbrk = T ML_Pretty.PrettyLineBreak;
+val fbrk = from_ML ML_Pretty.PrettyLineBreak;
+
+
+(* derived operations to create formatting expressions *)
 
 fun breaks prts = Library.separate (brk 1) prts;
 fun fbreaks prts = Library.separate fbrk prts;
 
 fun blk (indent, es) =

 
 fun output_spaces (ops: output_ops) = #output ops o Symbol.spaces;
 fun output_spaces_buffer ops = Buffer.add o #1 o output_spaces ops;
 
 
-(* formatted output *)
+(* output tree *)
+
+datatype tree =
+    Block of Markup.output * bool * int * tree list * int
+      (*markup output, consistent, indentation, body, length*)
+  | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
+  | Str of Output.output * int;  (*string output, length*)
+
+fun tree_length (Block (_, _, _, _, len)) = len
+  | tree_length (Break (_, wd, _)) = wd
+  | tree_length (Str (_, len)) = len;
 
 local
 
-type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
-
-val empty: text =
- {tx = Buffer.empty,
-  ind = Buffer.empty,
-  pos = 0,
-  nl = 0};
-
-fun newline s {tx, ind = _, pos = _, nl} : text =
- {tx = Buffer.add s tx,
-  ind = Buffer.empty,
-  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,
-  pos = pos + len,
-  nl = nl};
-
-(*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 (e :: es, after) = tree_length e + break_dist (es, after)
-  | break_dist ([], after) = after;
-
-val fbreak = Break (true, 1, 0);
-
-val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
-val force_all = map force_break;
-
-(*Search for the next break (at this or higher levels) and force it to occur.*)
-fun force_next [] = []
-  | force_next ((e as Break _) :: es) = force_break e :: es
-  | force_next (e :: es) = e :: force_next es;
+fun context_property context name =
+  let
+    fun get (ML_Pretty.ContextProperty (a, b)) = if name = a then SOME b else NONE
+      | get _ = NONE;
+  in the_default "" (get_first get context) end;
 
 fun block_length indent =
   let
     fun block_len len prts =
       let

             block_len len' (Break (false, indent + ind, 0) :: rest')
         | [] => len')
       end;
   in block_len 0 end;
 
-fun property context name =
-  let
-    fun get (ML_Pretty.ContextProperty (a, b)) = if name = a then SOME b else NONE
-      | get _ = NONE;
-  in the_default "" (get_first get context) end;
+val fbreak = Break (true, 1, 0);
 
 in
 
 fun output_tree (ops: output_ops) make_length =
   let
-    fun out (T (ML_Pretty.PrettyBlock (ind, consistent, context, body))) =
+    fun out (ML_Pretty.PrettyBlock (ind, consistent, context, body)) =
           let
-            val bg = property context "begin";
-            val en = property context "end";
+            val bg = context_property context "begin";
+            val en = context_property context "end";
             val m = #markup ops (bg, en);
             val indent = long_nat ind;
-            val body' = map (out o T) body;
+            val body' = map out body;
             val len = if make_length then block_length indent body' else ~1;
           in Block (m, consistent, indent, body', len) end
-      | out (T (ML_Pretty.PrettyBreak (wd, ind))) = Break (false, long_nat wd, long_nat ind)
-      | out (T ML_Pretty.PrettyLineBreak) = fbreak
-      | out (T (ML_Pretty.PrettyString s)) = Str (#output ops s ||> force_nat)
-      | out (T (ML_Pretty.PrettyStringWithWidth (s, n))) = Str (s, long_nat n);
-  in out end;
+      | out (ML_Pretty.PrettyBreak (wd, ind)) = Break (false, long_nat wd, long_nat ind)
+      | out ML_Pretty.PrettyLineBreak = fbreak
+      | out (ML_Pretty.PrettyString s) = Str (#output ops s ||> force_nat)
+      | out (ML_Pretty.PrettyStringWithWidth (s, n)) = Str (s, long_nat n);
+  in out o to_ML end;
+
+end;
+
+
+(* formatted output *)
+
+local
+
+type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
+
+val empty: text =
+ {tx = Buffer.empty,
+  ind = Buffer.empty,
+  pos = 0,
+  nl = 0};
+
+fun newline s {tx, ind = _, pos = _, nl} : text =
+ {tx = Buffer.add s tx,
+  ind = Buffer.empty,
+  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,
+  pos = pos + len,
+  nl = nl};
+
+(*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 (e :: es, after) = tree_length e + break_dist (es, after)
+  | break_dist ([], after) = after;
+
+val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
+val force_all = map force_break;
+
+(*Search for the next break (at this or higher levels) and force it to occur.*)
+fun force_next [] = []
+  | force_next ((e as Break _) :: es) = force_break e :: es
+  | force_next (e :: es) = e :: force_next es;
+
+in
 
 fun format_tree (ops: output_ops) input =
   let
     val margin = #margin ops;
     val breakgain = margin div 20;     (*minimum added space required of a break*)

   end;
 
 end;
 
 
-(*symbolic markup -- no formatting*)
+
+(** no formatting **)
+
+(* symbolic output: XML markup for blocks/breaks + other markup *)
+
 val symbolic =
   let
     val ops = markup_output_ops NONE;
 
     fun markup_buffer m body =

           markup_buffer (Markup.break wd ind) (output_spaces_buffer ops wd)
       | out (Break (true, _, _)) = Buffer.add (output_newline ops)
       | out (Str (s, _)) = Buffer.add s;
   in Buffer.build o out o output_tree ops false end;
 
-(*unformatted output*)
+val symbolic_output = Buffer.contents o symbolic;
+val symbolic_string_of = implode o symbolic_output;
+
+
+(* unformatted output: other markup only *)
+
 fun unformatted ops =
   let
     fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
       | out (Break (_, wd, _)) = output_spaces_buffer ops wd
       | out (Str (s, _)) = Buffer.add s;
   in Buffer.build o out o output_tree ops false end;
 
+fun unformatted_string_of prt =
+  let val ops = output_ops NONE
+  in implode (#escape ops (Buffer.contents (unformatted ops prt))) end;
+
 
 (* output interfaces *)
 
 val regularN = "pretty_regular";
 val symbolicN = "pretty_symbolic";

 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
 fun writeln prt =
   let val ops = output_ops NONE
   in Output.writelns (#escape ops (output ops prt)) end;
-
-val symbolic_output = Buffer.contents o symbolic;
-val symbolic_string_of = implode o symbolic_output;
-
-fun unformatted_string_of prt =
-  let val ops = output_ops NONE
-  in implode (#escape ops (Buffer.contents (unformatted ops prt))) end;
 
 
 (* chunks *)
 
 fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));

         [string_of_text_fold last])
       |> Output.writelns);
 
 end;
 
-end;
+
+
+(** back-patching **)
 
 structure ML_Pretty: ML_PRETTY =
 struct
   open ML_Pretty;
   val string_of = Pretty.string_of o Pretty.from_ML;