1 (* Title: Pure/General/pretty.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Author: Markus Wenzel, TU Munich
5 License: GPL (GNU GENERAL PUBLIC LICENSE)
7 Generic pretty printing module.
10 D. C. Oppen, "Pretty Printing",
11 ACM Transactions on Programming Languages and Systems (1980), 465-483.
13 The object to be printed is given as a tree with indentation and line
14 breaking information. A "break" inserts a newline if the text until
15 the next break is too long to fit on the current line. After the newline,
16 text is indented to the level of the enclosing block. Normally, if a block
17 is broken then all enclosing blocks will also be broken. Only "inconsistent
20 The stored length of a block is used in breakdist (to treat each inner block as
24 type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
25 (unit -> unit) * (unit -> unit);
30 val raw_str: string * real -> T
34 val blk: int * T list -> T
35 val unbreakable: T -> T
37 val commas: T list -> T list
38 val breaks: T list -> T list
39 val fbreaks: T list -> T list
40 val block: T list -> T
41 val strs: string list -> T
42 val enclose: string -> string -> T list -> T
43 val list: 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 writeln: T -> unit
50 val writelns: T list -> unit
51 val str_of: T -> string
52 val pprint: T -> pprint_args -> unit
53 val setdepth: int -> unit
54 val setmargin: int -> unit
55 val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
57 val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
59 val term: pp -> term -> T
60 val typ: pp -> typ -> T
61 val sort: pp -> sort -> T
62 val classrel: pp -> class list -> T
63 val arity: pp -> arity -> T
64 val string_of_term: pp -> term -> string
65 val string_of_typ: pp -> typ -> string
66 val string_of_sort: pp -> sort -> string
67 val string_of_classrel: pp -> class list -> string
68 val string_of_arity: pp -> arity -> string
71 structure Pretty : PRETTY =
75 (** printing items: compound phrases, strings, and breaks **)
78 Block of T list * int * int | (*body, indentation, length*)
79 String of string * int | (*text, length*)
80 Break of bool * int; (*mandatory flag, width if not taken*);
86 val output_spaces = Output.output o Symbol.spaces;
87 val add_indent = Buffer.add o output_spaces;
88 fun set_indent wd = Buffer.empty |> add_indent wd;
96 fun newline {tx, ind, pos, nl} =
97 {tx = Buffer.add (Output.output "\n") tx,
102 fun string (s, len) {tx, ind, pos: int, nl} =
103 {tx = Buffer.add s tx,
104 ind = Buffer.add s ind,
108 fun blanks wd = string (output_spaces wd, wd);
110 fun indentation (buf, len) {tx, ind, pos, nl} =
111 let val s = Buffer.content buf in
112 {tx = Buffer.add (Output.indent (s, len)) tx,
113 ind = Buffer.add s ind,
124 fun make_margin_info m =
125 {margin = m, (*right margin, or page width*)
126 breakgain = m div 20, (*minimum added space required of a break*)
127 emergencypos = m div 2}; (*position too far to right*)
129 val margin_info = ref (make_margin_info 76);
130 fun setmargin m = margin_info := make_margin_info m;
131 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
136 (*Add the lengths of the expressions until the next Break; if no Break then
137 include "after", to account for text following this block.*)
138 fun breakdist (Block (_, _, len) :: es, after) = len + breakdist (es, after)
139 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
140 | breakdist (Break _ :: es, after) = 0
141 | breakdist ([], after) = after;
143 (*Search for the next break (at this or higher levels) and force it to occur.*)
144 fun forcenext [] = []
145 | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
146 | forcenext (e :: es) = e :: forcenext es;
148 (*es is list of expressions to print;
149 blockin is the indentation of the current block;
150 after is the width of the following context until next break.*)
151 fun format ([], _, _) text = text
152 | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
154 Block (bes, indent, wd) =>
156 val {emergencypos, ...} = ! margin_info;
157 val pos' = pos + indent;
158 val pos'' = pos' mod emergencypos;
160 if pos' < emergencypos then (ind |> add_indent indent, pos')
161 else (set_indent pos'', pos'');
162 val btext = format (bes, block', breakdist (es, after)) text;
163 (*if this block was broken then force the next break*)
164 val es2 = if nl < #nl btext then forcenext es else es;
165 in format (es2, block, after) btext end
166 | String str => format (es, block, after) (string str text)
167 | Break (force, wd) =>
168 let val {margin, breakgain, ...} = ! margin_info in
169 (*no break if text to next break fits on this line
170 or if breaking would add only breakgain to space*)
171 format (es, block, after)
172 (if not force andalso
173 pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
174 then text |> blanks wd (*just insert wd blanks*)
175 else text |> newline |> indentation block)
179 (** Exported functions to create formatting expressions **)
181 fun length (Block (_, _, len)) = len
182 | length (String (_, len)) = len
183 | length (Break(_, wd)) = wd;
185 fun raw_str (s, len) = String (s, Real.round len);
186 val str = String o apsnd Real.round o Output.output_width;
188 fun brk wd = Break (false, wd);
189 val fbrk = Break (true, 2);
191 fun blk (indent, es) =
194 | sum(e :: es, k) = sum (es, length e + k);
195 in Block (es, indent, sum (es, 0)) end;
197 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
198 | unbreakable (Block (es, indent, wd)) = Block (map unbreakable es, indent, wd)
199 | unbreakable (e as String _) = e;
205 blk (1, [str "\"", prt, str "\""]);
208 flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
210 fun breaks prts = separate (brk 1) prts;
211 fun fbreaks prts = separate fbrk prts;
213 fun block prts = blk (2, prts);
215 val strs = block o breaks o map str;
217 fun enclose lpar rpar prts =
218 block (str lpar :: (prts @ [str rpar]));
220 fun list lpar rpar prts = enclose lpar rpar (commas prts);
221 fun str_list lpar rpar strs = list lpar rpar (map str strs);
222 fun big_list name prts = block (fbreaks (str name :: prts));
223 fun chunks prts = blk (0, fbreaks prts);
225 fun indent 0 prt = prt
226 | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
230 (** Pretty printing with depth limitation **)
232 val depth = ref 0; (*maximum depth; 0 means no limit*)
234 fun setdepth dp = (depth := dp);
236 (*Recursively prune blocks, discarding all text exceeding depth dp*)
237 fun pruning dp (Block(bes,indent,wd)) =
238 if dp>0 then blk(indent, map (pruning(dp-1)) bes)
242 fun prune dp e = if dp > 0 then pruning dp e else e;
245 Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty))
248 val writeln = writeln o string_of;
249 fun writelns [] = () | writelns es = writeln (chunks es);
252 (*Create a single flat string: no line breaking*)
255 fun s_of (Block (prts, _, _)) = implode (map s_of prts)
256 | s_of (String (s, _)) = s
257 | s_of (Break (false, wd)) = output_spaces wd
258 | s_of (Break (true, _)) = output_spaces 1;
259 in Output.raw (s_of (prune (! depth) prt)) end;
261 (*part of the interface to the ML toplevel pretty printers*)
262 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
264 fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
265 | pp (String (s, _)) = put_str s
266 | pp (Break (false, wd)) = put_brk wd
267 | pp (Break (true, _)) = put_fbrk ()
269 | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
271 pp (prune (! depth) prt)
276 (** abstract pretty printing context **)
279 PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
283 fun pp_fun f (PP x) = f x;
285 val term = pp_fun #1;
287 val sort = pp_fun #3;
288 val classrel = pp_fun #4;
289 val arity = pp_fun #5;
291 val string_of_term = string_of oo term;
292 val string_of_typ = string_of oo typ;
293 val string_of_sort = string_of oo sort;
294 val string_of_classrel = string_of oo classrel;
295 val string_of_arity = string_of oo arity;
297 fun undef kind _ = str ("*** UNABLE TO PRINT " ^ kind ^ " ***");
299 pp (undef "term", undef "typ", undef "sort", undef "classrel", undef "arity");