1 (* Title: Pure/General/pretty.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Author: Markus Wenzel, TU Munich
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);
29 val raw_str: string * real -> T
33 val blk: int * T list -> T
34 val unbreakable: T -> T
36 val commas: T list -> T list
37 val breaks: T list -> T list
38 val fbreaks: T list -> T list
39 val block: T list -> T
40 val strs: string list -> T
41 val enclose: string -> string -> T list -> T
42 val list: string -> string -> T list -> T
43 val gen_list: string -> string -> string -> T list -> T
44 val str_list: string -> string -> string list -> T
45 val big_list: string -> T list -> T
46 val chunks: T list -> T
47 val indent: int -> T -> T
48 val string_of: T -> string
49 val output_buffer: T -> Buffer.T
50 val output: T -> string
51 val writeln: T -> unit
52 val writelns: T list -> unit
53 val str_of: T -> string
54 val pprint: T -> pprint_args -> unit
55 val setdepth: int -> unit
56 val setmargin: int -> unit
57 val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
59 val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
60 val term: pp -> term -> T
61 val typ: pp -> typ -> T
62 val sort: pp -> sort -> T
63 val classrel: pp -> class list -> T
64 val arity: pp -> arity -> T
65 val string_of_term: pp -> term -> string
66 val string_of_typ: pp -> typ -> string
67 val string_of_sort: pp -> sort -> string
68 val string_of_classrel: pp -> class list -> string
69 val string_of_arity: pp -> arity -> string
72 structure Pretty : PRETTY =
76 (** printing items: compound phrases, strings, and breaks **)
79 Block of T list * int * int | (*body, indentation, length*)
80 String of string * int | (*text, length*)
81 Break of bool * int; (*mandatory flag, width if not taken*)
87 val output_spaces = Output.output o Symbol.spaces;
88 val add_indent = Buffer.add o output_spaces;
89 fun set_indent wd = Buffer.empty |> add_indent wd;
91 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
99 fun newline {tx, ind, pos, nl} : text =
100 {tx = Buffer.add (Output.output "\n") tx,
105 fun string (s, len) {tx, ind, pos: int, nl} : text =
106 {tx = Buffer.add s tx,
107 ind = Buffer.add s ind,
111 fun blanks wd = string (output_spaces wd, wd);
113 fun indentation (buf, len) {tx, ind, pos, nl} : text =
114 let val s = Buffer.content buf in
115 {tx = Buffer.add (Output.indent (s, len)) tx,
116 ind = Buffer.add s ind,
127 fun make_margin_info m =
128 {margin = m, (*right margin, or page width*)
129 breakgain = m div 20, (*minimum added space required of a break*)
130 emergencypos = m div 2}; (*position too far to right*)
132 val margin_info = ref (make_margin_info 76);
133 fun setmargin m = margin_info := make_margin_info m;
134 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
139 (*Add the lengths of the expressions until the next Break; if no Break then
140 include "after", to account for text following this block.*)
141 fun breakdist (Block (_, _, len) :: es, after) = len + breakdist (es, after)
142 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
143 | breakdist (Break _ :: es, after) = 0
144 | breakdist ([], after) = after;
146 (*Search for the next break (at this or higher levels) and force it to occur.*)
147 fun forcenext [] = []
148 | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
149 | forcenext (e :: es) = e :: forcenext es;
151 (*es is list of expressions to print;
152 blockin is the indentation of the current block;
153 after is the width of the following context until next break.*)
154 fun format ([], _, _) text = text
155 | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
157 Block (bes, indent, wd) =>
159 val {emergencypos, ...} = ! margin_info;
160 val pos' = pos + indent;
161 val pos'' = pos' mod emergencypos;
163 if pos' < emergencypos then (ind |> add_indent indent, pos')
164 else (set_indent pos'', pos'');
165 val btext: text = format (bes, block', breakdist (es, after)) text;
166 (*if this block was broken then force the next break*)
167 val es2 = if nl < #nl btext then forcenext es else es;
168 in format (es2, block, after) btext end
169 | String str => format (es, block, after) (string str text)
170 | Break (force, wd) =>
171 let val {margin, breakgain, ...} = ! margin_info in
172 (*no break if text to next break fits on this line
173 or if breaking would add only breakgain to space*)
174 format (es, block, after)
175 (if not force andalso
176 pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
177 then text |> blanks wd (*just insert wd blanks*)
178 else text |> newline |> indentation block)
182 (** Exported functions to create formatting expressions **)
184 fun length (Block (_, _, len)) = len
185 | length (String (_, len)) = len
186 | length (Break(_, wd)) = wd;
188 fun raw_str (s, len) = String (s, Real.round len);
189 val str = String o apsnd Real.round o Output.output_width;
191 fun brk wd = Break (false, wd);
192 val fbrk = Break (true, 2);
194 fun blk (indent, es) =
197 | sum(e :: es, k) = sum (es, length e + k);
198 in Block (es, indent, sum (es, 0)) end;
200 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
201 | unbreakable (Block (es, indent, wd)) = Block (map unbreakable es, indent, wd)
202 | unbreakable (e as String _) = e;
208 blk (1, [str "\"", prt, str "\""]);
210 fun separate_pretty sep prts =
213 |> separate [str sep, brk 1]
216 val commas = separate_pretty ",";
218 fun breaks prts = separate (brk 1) prts;
219 fun fbreaks prts = separate fbrk prts;
221 fun block prts = blk (2, prts);
223 val strs = block o breaks o map str;
225 fun enclose lpar rpar prts =
226 block (str lpar :: (prts @ [str rpar]));
228 fun gen_list sep lpar rpar prts = enclose lpar rpar (separate_pretty sep prts);
229 val list = gen_list ",";
230 fun str_list lpar rpar strs = list lpar rpar (map str strs);
231 fun big_list name prts = block (fbreaks (str name :: prts));
232 fun chunks prts = blk (0, fbreaks prts);
234 fun indent 0 prt = prt
235 | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
239 (** Pretty printing with depth limitation **)
241 val depth = ref 0; (*maximum depth; 0 means no limit*)
243 fun setdepth dp = (depth := dp);
245 (*Recursively prune blocks, discarding all text exceeding depth dp*)
246 fun pruning dp (Block(bes,indent,wd)) =
247 if dp>0 then blk(indent, map (pruning(dp-1)) bes)
251 fun prune dp e = if dp > 0 then pruning dp e else e;
253 fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty);
254 val output = Buffer.content o output_buffer;
255 val string_of = Output.raw o output;
256 val writeln = Output.writeln o string_of;
257 fun writelns [] = () | writelns es = writeln (chunks es);
260 (*Create a single flat string: no line breaking*)
263 fun s_of (Block (prts, _, _)) = implode (map s_of prts)
264 | s_of (String (s, _)) = s
265 | s_of (Break (false, wd)) = output_spaces wd
266 | s_of (Break (true, _)) = output_spaces 1;
267 in Output.raw (s_of (prune (! depth) prt)) end;
269 (*part of the interface to the ML toplevel pretty printers*)
270 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
272 fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
273 | pp (String (s, _)) = put_str s
274 | pp (Break (false, wd)) = put_brk wd
275 | pp (Break (true, _)) = put_fbrk ()
277 | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
279 pp (prune (! depth) prt)
284 (** abstract pretty printing context **)
287 PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
291 fun pp_fun f (PP x) = f x;
293 val term = pp_fun #1;
295 val sort = pp_fun #3;
296 val classrel = pp_fun #4;
297 val arity = pp_fun #5;
299 val string_of_term = string_of oo term;
300 val string_of_typ = string_of oo typ;
301 val string_of_sort = string_of oo sort;
302 val string_of_classrel = string_of oo classrel;
303 val string_of_arity = string_of oo arity;