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 = (output -> unit) * (int -> unit) * (int -> unit) *
24 (unit -> unit) * (unit -> unit);
28 val default_indent: string -> int -> output
29 val add_mode: string -> (string -> int -> output) -> unit
31 val raw_str: output * int -> T
35 val breaks: T list -> T list
36 val fbreaks: T list -> T list
37 val blk: int * T list -> T
38 val block: T list -> T
39 val strs: string list -> T
40 val markup: Markup.T -> T list -> T
41 val keyword: string -> T
42 val command: string -> T
43 val markup_chunks: Markup.T -> T list -> T
44 val chunks: T list -> T
45 val chunks2: T list -> T
46 val block_enclose: T * T -> T list -> T
49 val separate: string -> T list -> T list
50 val commas: T list -> T list
51 val enclose: string -> string -> T list -> T
52 val enum: string -> string -> string -> T list -> T
53 val list: string -> string -> T list -> T
54 val str_list: string -> string -> string list -> T
55 val big_list: string -> T list -> T
56 val indent: int -> T -> T
57 val unbreakable: T -> T
58 val setmargin: int -> unit
59 val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
60 val setdepth: int -> unit
61 val pprint: T -> pprint_args -> unit
63 val output_buffer: T -> Buffer.T
64 val output: T -> output
65 val string_of: T -> string
66 val str_of: T -> string
67 val writeln: T -> unit
69 val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
70 val term: pp -> term -> T
71 val typ: pp -> typ -> T
72 val sort: pp -> sort -> T
73 val classrel: pp -> class list -> T
74 val arity: pp -> arity -> T
75 val string_of_term: pp -> term -> string
76 val string_of_typ: pp -> typ -> string
77 val string_of_sort: pp -> sort -> string
78 val string_of_classrel: pp -> class list -> string
79 val string_of_arity: pp -> arity -> string
82 structure Pretty: PRETTY =
85 (** print mode operations **)
87 fun default_indent (_: string) = Symbol.spaces;
90 val default = {indent = default_indent};
91 val modes = ref (Symtab.make [("", default)]);
93 fun add_mode name indent =
94 change modes (Symtab.update_new (name, {indent = indent}));
96 the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
99 fun mode_indent x y = #indent (get_mode ()) x y;
101 val output_spaces = Output.output o Symbol.spaces;
102 val add_indent = Buffer.add o output_spaces;
106 (** printing items: compound phrases, strings, and breaks **)
109 Block of Markup.T * T list * int * int | (*markup, body, indentation, length*)
110 String of output * int | (*text, length*)
111 Break of bool * int; (*mandatory flag, width if not taken*)
113 fun length (Block (_, _, _, len)) = len
114 | length (String (_, len)) = len
115 | length (Break (_, wd)) = wd;
119 (** derived operations to create formatting expressions **)
121 val raw_str = String;
122 val str = String o Output.output_width;
124 fun brk wd = Break (false, wd);
125 val fbrk = Break (true, 2);
127 fun breaks prts = Library.separate (brk 1) prts;
128 fun fbreaks prts = Library.separate fbrk prts;
130 fun markup_block m (indent, es) =
133 | sum (e :: es) k = sum es (length e + k);
134 in Block (m, es, indent, sum es 0) end;
136 val blk = markup_block Markup.none;
137 fun block prts = blk (2, prts);
138 val strs = block o breaks o map str;
140 fun markup m prts = markup_block m (0, prts);
141 fun keyword name = markup (Markup.keyword name) [str name];
142 fun command name = markup (Markup.command name) [str name];
144 fun markup_chunks m prts = markup m (fbreaks prts);
145 val chunks = markup_chunks Markup.none;
146 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
148 fun block_enclose (p1, p2) ps = chunks [(block o fbreaks) (p1 :: ps), p2];
150 fun quote prt = blk (1, [str "\"", prt, str "\""]);
151 fun backquote prt = blk (1, [str "`", prt, str "`"]);
153 fun separate sep prts =
154 flat (Library.separate [str sep, brk 1] (map single prts));
156 val commas = separate ",";
158 fun enclose lpar rpar prts =
159 block (str lpar :: (prts @ [str rpar]));
161 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
164 fun str_list lpar rpar strs = list lpar rpar (map str strs);
166 fun big_list name prts = block (fbreaks (str name :: prts));
168 fun indent 0 prt = prt
169 | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
171 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
172 | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
173 | unbreakable (e as String _) = e;
181 fun make_margin_info m =
182 {margin = m, (*right margin, or page width*)
183 breakgain = m div 20, (*minimum added space required of a break*)
184 emergencypos = m div 2}; (*position too far to right*)
186 val margin_info = ref (make_margin_info 76);
187 fun setmargin m = margin_info := make_margin_info m;
188 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
191 (* depth limitation *)
193 val depth = ref 0; (*maximum depth; 0 means no limit*)
194 fun setdepth dp = (depth := dp);
197 fun pruning dp (Block (m, bes, indent, wd)) =
199 then markup_block m (indent, map (pruning (dp - 1)) bes)
203 fun prune e = if ! depth > 0 then pruning (! depth) e else e;
207 (* formatted output *)
211 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
219 fun newline {tx, ind, pos, nl} : text =
220 {tx = Buffer.add (Output.output "\n") tx,
225 fun control s {tx, ind, pos: int, nl} : text =
226 {tx = Buffer.add s tx,
231 fun string (s, len) {tx, ind, pos: int, nl} : text =
232 {tx = Buffer.add s tx,
233 ind = Buffer.add s ind,
237 fun blanks wd = string (output_spaces wd, wd);
239 fun indentation (buf, len) {tx, ind, pos, nl} : text =
240 let val s = Buffer.content buf in
241 {tx = Buffer.add (mode_indent s len) tx,
242 ind = Buffer.add s ind,
247 (*Add the lengths of the expressions until the next Break; if no Break then
248 include "after", to account for text following this block.*)
249 fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
250 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
251 | breakdist (Break _ :: es, after) = 0
252 | breakdist ([], after) = after;
254 (*Search for the next break (at this or higher levels) and force it to occur.*)
255 fun forcenext [] = []
256 | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
257 | forcenext (e :: es) = e :: forcenext es;
259 (*es is list of expressions to print;
260 blockin is the indentation of the current block;
261 after is the width of the following context until next break.*)
262 fun format ([], _, _) text = text
263 | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
265 Block (markup, bes, indent, wd) =>
267 val {emergencypos, ...} = ! margin_info;
268 val pos' = pos + indent;
269 val pos'' = pos' mod emergencypos;
271 if pos' < emergencypos then (ind |> add_indent indent, pos')
272 else (add_indent pos'' Buffer.empty, pos'');
273 val (bg, en) = Markup.output markup;
274 val btext: text = text
276 |> format (bes, block', breakdist (es, after))
278 (*if this block was broken then force the next break*)
279 val es' = if nl < #nl btext then forcenext es else es;
280 in format (es', block, after) btext end
281 | String str => format (es, block, after) (string str text)
282 | Break (force, wd) =>
283 let val {margin, breakgain, ...} = ! margin_info in
284 (*no break if text to next break fits on this line
285 or if breaking would add only breakgain to space*)
286 format (es, block, after)
287 (if not force andalso
288 pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
289 then text |> blanks wd (*just insert wd blanks*)
290 else text |> newline |> indentation block)
295 fun formatted e = #tx (format ([prune e], (Buffer.empty, 0), 0) empty);
302 (*symbolic markup -- no formatting*)
305 fun out (Block (m, [], _, _)) = Buffer.markup m I
306 | out (Block (m, prts, indent, _)) =
307 Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts))
308 | out (String (s, _)) = Buffer.add s
309 | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
310 | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
311 in out prt Buffer.empty end;
313 (*unformatted output*)
314 fun unformatted prt =
316 fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts)
317 | fmt (String (s, _)) = Buffer.add s
318 | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
319 | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
320 in fmt (prune prt) Buffer.empty end;
322 (*ML toplevel pretty printing*)
323 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
325 fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
326 | pp (String (s, _)) = put_str s
327 | pp (Break (false, wd)) = put_brk wd
328 | pp (Break (true, _)) = put_fbrk ()
330 | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
331 in pp (prune prt) end;
334 (* output interfaces *)
336 val symbolicN = "pretty_symbolic";
338 fun output_buffer prt =
339 if print_mode_active symbolicN then symbolic prt
342 val output = Buffer.content o output_buffer;
343 val string_of = Output.escape o output;
344 val str_of = Output.escape o Buffer.content o unformatted;
345 val writeln = Output.writeln o string_of;
349 (** abstract pretty printing context **)
352 PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
356 fun pp_fun f (PP x) = f x;
358 val term = pp_fun #1;
360 val sort = pp_fun #3;
361 val classrel = pp_fun #4;
362 val arity = pp_fun #5;
364 val string_of_term = string_of oo term;
365 val string_of_typ = string_of oo typ;
366 val string_of_sort = string_of oo sort;
367 val string_of_classrel = string_of oo classrel;
368 val string_of_arity = string_of oo arity;