1 (* Title: Pure/General/pretty.ML
3 Author: Lawrence C Paulson
4 Copyright 1991 University of Cambridge
6 Generic pretty printing module.
9 D. C. Oppen, "Pretty Printing",
10 ACM Transactions on Programming Languages and Systems (1980), 465-483.
12 The object to be printed is given as a tree with indentation and line
13 breaking information. A "break" inserts a newline if the text until
14 the next break is too long to fit on the current line. After the newline,
15 text is indented to the level of the enclosing block. Normally, if a block
16 is broken then all enclosing blocks will also be broken. Only "inconsistent
19 The stored length of a block is used in breakdist (to treat each inner block as
23 type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
24 (unit -> unit) * (unit -> unit);
30 val strlen: string -> int -> T
35 val blk: int * T list -> T
36 val lst: string * string -> T list -> T
38 val commas: T list -> T list
39 val breaks: T list -> T list
40 val fbreaks: T list -> T list
41 val block: T list -> T
42 val strs: string list -> T
43 val enclose: string -> string -> T list -> T
44 val list: string -> string -> T list -> T
45 val str_list: string -> string -> string list -> T
46 val big_list: string -> T list -> T
47 val string_of: T -> string
48 val writeln: T -> unit
49 val str_of: T -> string
50 val pprint: T -> pprint_args -> unit
51 val setdepth: int -> unit
52 val setmargin: int -> unit
55 structure Pretty : PRETTY =
58 (*printing items: compound phrases, strings, and breaks*)
60 Block of T list * int * int | (*body, indentation, length*)
61 String of string * int | (*text, length*)
62 Break of bool * int; (*mandatory flag, width if not taken*);
64 (*Add the lengths of the expressions until the next Break; if no Break then
65 include "after", to account for text following this block. *)
66 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
67 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
68 | breakdist (Break _ :: es, after) = 0
69 | breakdist ([], after) = after;
71 fun repstring a 0 = ""
74 if k mod 2 = 0 then repstring(a^a) (k div 2)
75 else repstring(a^a) (k div 2) ^ a;
77 (*** Type for lines of text: string, # of lines, position on line ***)
79 type text = {tx: string, nl: int, pos: int};
81 val emptytext = {tx="", nl=0, pos=0};
83 fun blanks wd {tx,nl,pos} =
84 {tx = tx ^ repstring " " wd,
88 fun newline {tx,nl,pos} =
93 fun string s len {tx,nl,pos:int} =
104 val margin = ref 80 (*right margin, or page width*)
105 and breakgain = ref 4 (*minimum added space required of a break*)
106 and emergencypos = ref 40; (*position too far to right*)
110 breakgain := !margin div 20;
111 emergencypos := !margin div 2);
113 val () = setmargin 76;
116 (*Search for the next break (at this or higher levels) and force it to occur*)
117 fun forcenext [] = []
118 | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
119 | forcenext (e :: es) = e :: forcenext es;
121 (*es is list of expressions to print;
122 blockin is the indentation of the current block;
123 after is the width of the following context until next break. *)
124 fun format ([], _, _) text = text
125 | format (e::es, blockin, after) (text as {pos,nl,...}) =
127 Block(bes,indent,wd) =>
128 let val blockin' = (pos + indent) mod !emergencypos
129 val btext = format(bes, blockin', breakdist(es,after)) text
130 (*If this block was broken then force the next break.*)
131 val es2 = if nl < #nl(btext) then forcenext es else es
132 in format (es2,blockin,after) btext end
133 | String (s, len) => format (es,blockin,after) (string s len text)
134 | Break(force,wd) => (*no break if text to next break fits on this line
135 or if breaking would add only breakgain to space *)
136 format (es,blockin,after)
137 (if not force andalso
138 pos+wd <= Int.max(!margin - breakdist(es,after),
139 blockin + !breakgain)
140 then blanks wd text (*just insert wd blanks*)
141 else blanks blockin (newline text)));
144 (*** Exported functions to create formatting expressions ***)
146 fun length (Block (_, _, len)) = len
147 | length (String (_, len)) = len
148 | length (Break(_, wd)) = wd;
150 fun str s = String (s, size s);
151 fun strlen s len = String (s, len);
152 fun sym s = String (s, Symbol.size s);
154 fun spc n = str (repstring " " n);
156 fun brk wd = Break (false, wd);
157 val fbrk = Break (true, 0);
159 fun blk (indent, es) =
162 | sum(e :: es, k) = sum (es, length e + k);
163 in Block (es, indent, sum (es, 0)) end;
165 (*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
167 let fun add(e,es) = str"," :: brk 1 :: e :: es;
168 fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
169 | list(e::[]) = [str lp, e, str rp]
171 in blk(size lp, list es) end;
177 blk (1, [str "\"", prt, str "\""]);
180 flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
182 fun breaks prts = separate (brk 1) prts;
184 fun fbreaks prts = separate fbrk prts;
186 fun block prts = blk (2, prts);
188 val strs = block o breaks o (map str);
190 fun enclose lpar rpar prts =
191 block (str lpar :: (prts @ [str rpar]));
193 fun list lpar rpar prts =
194 enclose lpar rpar (commas prts);
196 fun str_list lpar rpar strs =
197 list lpar rpar (map str strs);
199 fun big_list name prts =
200 block (fbreaks (str name :: prts));
204 (*** Pretty printing with depth limitation ***)
206 val depth = ref 0; (*maximum depth; 0 means no limit*)
208 fun setdepth dp = (depth := dp);
210 (*Recursively prune blocks, discarding all text exceeding depth dp*)
211 fun pruning dp (Block(bes,indent,wd)) =
212 if dp>0 then blk(indent, map (pruning(dp-1)) bes)
216 fun prune dp e = if dp>0 then pruning dp e else e;
219 fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
221 val writeln = writeln o string_of;
224 (*Create a single flat string: no line breaking*)
227 fun s_of (Block (prts, _, _)) = implode (map s_of prts)
228 | s_of (String (s, _)) = s
229 | s_of (Break (false, wd)) = repstring " " wd
230 | s_of (Break (true, _)) = " ";
232 s_of (prune (! depth) prt)
235 (*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
236 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
238 fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
239 | pp (String (s, _)) = put_str s
240 | pp (Break (false, wd)) = put_brk wd
241 | pp (Break (true, _)) = put_fbrk ()
243 | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
245 pp (prune (! depth) prt)