src/Pure/General/pretty.ML
changeset 8456 8ccda76f07cb
parent 6321 207f518167e8
child 8806 a202293db3f6
     1.1 --- a/src/Pure/General/pretty.ML	Wed Mar 15 12:05:03 2000 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Wed Mar 15 18:18:12 2000 +0100
     1.3 @@ -26,15 +26,11 @@
     1.4  signature PRETTY =
     1.5    sig
     1.6    type T
     1.7 +  val raw_str: string * real -> T
     1.8    val str: string -> T
     1.9 -  val strlen: string -> int -> T
    1.10 -  val strlen_real: string -> real -> T
    1.11 -  val sym: string -> T
    1.12 -  val spc: int -> T
    1.13    val brk: int -> T
    1.14    val fbrk: T
    1.15    val blk: int * T list -> T
    1.16 -  val lst: string * string -> T list -> T
    1.17    val quote: T -> T
    1.18    val commas: T list -> T list
    1.19    val breaks: T list -> T list
    1.20 @@ -45,6 +41,7 @@
    1.21    val list: string -> string -> T list -> T
    1.22    val str_list: string -> string -> string list -> T
    1.23    val big_list: string -> T list -> T
    1.24 +  val chunks: T list -> T
    1.25    val string_of: T -> string
    1.26    val writeln: T -> unit
    1.27    val str_of: T -> string
    1.28 @@ -78,22 +75,22 @@
    1.29  
    1.30  (*** Type for lines of text: string, # of lines, position on line ***)
    1.31  
    1.32 -type text = {tx: string, nl: int, pos: int};
    1.33 +type text = {tx: Buffer.T, nl: int, pos: int};
    1.34  
    1.35 -val emptytext = {tx="", nl=0, pos=0};
    1.36 +val emptytext = {tx = Buffer.empty, nl = 0, pos = 0};
    1.37  
    1.38 -fun blanks wd {tx,nl,pos} =
    1.39 -    {tx  = tx ^ repstring " " wd,
    1.40 +fun blanks wd {tx, nl, pos} =
    1.41 +    {tx  = Buffer.add (Symbol.output (repstring " " wd)) tx,
    1.42       nl  = nl,
    1.43       pos = pos+wd};
    1.44  
    1.45 -fun newline {tx,nl,pos} =
    1.46 -    {tx  = tx ^ "\n",
    1.47 -     nl  = nl+1,
    1.48 +fun newline {tx, nl, pos} =
    1.49 +    {tx  = Buffer.add (Symbol.output "\n") tx,
    1.50 +     nl  = nl + 1,
    1.51       pos = 0};
    1.52  
    1.53 -fun string s len {tx,nl,pos:int} =
    1.54 -    {tx  = tx ^ s,
    1.55 +fun string s len {tx, nl, pos:int} =
    1.56 +    {tx  = Buffer.add s tx,
    1.57       nl  = nl,
    1.58       pos = pos + len};
    1.59  
    1.60 @@ -145,12 +142,8 @@
    1.61    | length (String (_, len)) = len
    1.62    | length (Break(_, wd)) = wd;
    1.63  
    1.64 -fun str s = String (s, size s);
    1.65 -fun strlen s len = String (s, len);
    1.66 -fun strlen_real s len = strlen s (Real.round len);
    1.67 -val sym = String o apsnd Real.round o Symbol.output_width;
    1.68 -
    1.69 -fun spc n = str (repstring " " n);
    1.70 +fun raw_str (s, len) = String (s, Real.round len);
    1.71 +val str = String o apsnd Real.round o Symbol.output_width;
    1.72  
    1.73  fun brk wd = Break (false, wd);
    1.74  val fbrk = Break (true, 0);
    1.75 @@ -161,14 +154,6 @@
    1.76        | sum(e :: es, k) = sum (es, length e + k);
    1.77    in Block (es, indent, sum (es, 0)) end;
    1.78  
    1.79 -(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
    1.80 -fun lst(lp,rp) es =
    1.81 -  let fun add(e,es) = str"," :: brk 1 :: e :: es;
    1.82 -      fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
    1.83 -        | list(e::[]) = [str lp, e, str rp]
    1.84 -        | list([]) = []
    1.85 -  in blk(size lp, list es) end;
    1.86 -
    1.87  
    1.88  (* utils *)
    1.89  
    1.90 @@ -179,7 +164,6 @@
    1.91    flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
    1.92  
    1.93  fun breaks prts = separate (brk 1) prts;
    1.94 -
    1.95  fun fbreaks prts = separate fbrk prts;
    1.96  
    1.97  fun block prts = blk (2, prts);
    1.98 @@ -189,15 +173,10 @@
    1.99  fun enclose lpar rpar prts =
   1.100    block (str lpar :: (prts @ [str rpar]));
   1.101  
   1.102 -fun list lpar rpar prts =
   1.103 -  enclose lpar rpar (commas prts);
   1.104 -
   1.105 -fun str_list lpar rpar strs =
   1.106 -  list lpar rpar (map str strs);
   1.107 -
   1.108 -fun big_list name prts =
   1.109 -  block (fbreaks (str name :: prts));
   1.110 -
   1.111 +fun list lpar rpar prts = enclose lpar rpar (commas prts);
   1.112 +fun str_list lpar rpar strs = list lpar rpar (map str strs);
   1.113 +fun big_list name prts = block (fbreaks (str name :: prts));
   1.114 +fun chunks prts = blk (0, fbreaks prts);
   1.115  
   1.116  
   1.117  (*** Pretty printing with depth limitation ***)
   1.118 @@ -215,7 +194,7 @@
   1.119  fun prune dp e = if dp>0 then pruning dp e else e;
   1.120  
   1.121  
   1.122 -fun string_of e = #tx (format ([prune (! depth) e], 0, 0) emptytext);
   1.123 +fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], 0, 0) emptytext));
   1.124  
   1.125  val writeln = writeln o string_of;
   1.126  
   1.127 @@ -225,11 +204,11 @@
   1.128    let
   1.129      fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   1.130        | s_of (String (s, _)) = s
   1.131 -      | s_of (Break (false, wd)) = repstring " " wd
   1.132 -      | s_of (Break (true, _)) = " ";
   1.133 +      | s_of (Break (false, wd)) = Symbol.output (repstring " " wd)
   1.134 +      | s_of (Break (true, _)) = Symbol.output " ";
   1.135    in s_of (prune (! depth) prt) end;
   1.136  
   1.137 -(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
   1.138 +(*part of the interface to the ML toplevel pretty printers*)
   1.139  fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   1.140    let
   1.141      fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())