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);
28 val default_indent: string -> int -> string
29 val default_markup: Markup.T -> string * string
30 val add_mode: string -> (string -> int -> string) -> (Markup.T -> string * string) -> unit
32 val raw_str: string * int -> T
36 val blk: int * T list -> T
37 val unbreakable: T -> T
38 val breaks: T list -> T list
39 val fbreaks: T list -> T list
40 val block: T list -> T
41 val markup: Markup.T -> T list -> T
42 val keyword: string -> T
43 val command: string -> T
44 val strs: string list -> T
45 val chunks: T list -> T
46 val chunks2: T list -> T
47 val block_enclose: T * T -> T list -> T
50 val separate: string -> T list -> T list
51 val commas: T list -> T list
52 val enclose: string -> string -> T list -> T
53 val enum: string -> string -> string -> T list -> T
54 val list: string -> string -> T list -> T
55 val str_list: string -> string -> string list -> T
56 val big_list: string -> T list -> T
57 val indent: int -> T -> T
58 val string_of: T -> string
59 val output_buffer: T -> Buffer.T
60 val output: T -> string
61 val writeln: T -> unit
62 val str_of: T -> string
63 val pprint: T -> pprint_args -> unit
64 val setdepth: int -> unit
65 val setmargin: int -> unit
66 val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
68 val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
69 val term: pp -> term -> T
70 val typ: pp -> typ -> T
71 val sort: pp -> sort -> T
72 val classrel: pp -> class list -> T
73 val arity: pp -> arity -> T
74 val string_of_term: pp -> term -> string
75 val string_of_typ: pp -> typ -> string
76 val string_of_sort: pp -> sort -> string
77 val string_of_classrel: pp -> class list -> string
78 val string_of_arity: pp -> arity -> string
81 structure Pretty: PRETTY =
84 (** print mode operations **)
86 fun default_indent (_: string) = Symbol.spaces;
87 fun default_markup (_: Markup.T) = ("", "");
90 val default = {indent = default_indent, markup = default_markup};
91 val modes = ref (Symtab.make [("", default)]);
93 fun add_mode name indent markup =
94 change modes (Symtab.update_new (name, {indent = indent, markup = markup}));
96 the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
99 fun mode_indent x y = #indent (get_mode ()) x y;
100 fun mode_markup x = #markup (get_mode ()) x;
104 (** printing items: compound phrases, strings, and breaks **)
107 Block of Markup.T * T list * int * int | (*markup, body, indentation, length*)
108 String of string * int | (*text, length*)
109 Break of bool * int; (*mandatory flag, width if not taken*)
115 val output_spaces = Output.output o Symbol.spaces;
116 val add_indent = Buffer.add o output_spaces;
117 fun set_indent wd = Buffer.empty |> add_indent wd;
119 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
127 fun newline {tx, ind, pos, nl} : text =
128 {tx = Buffer.add (Output.output "\n") tx,
133 fun control s {tx, ind, pos: int, nl} : text =
134 {tx = Buffer.add s tx,
139 fun string (s, len) {tx, ind, pos: int, nl} : text =
140 {tx = Buffer.add s tx,
141 ind = Buffer.add s ind,
145 fun blanks wd = string (output_spaces wd, wd);
147 fun indentation (buf, len) {tx, ind, pos, nl} : text =
148 let val s = Buffer.content buf in
149 {tx = Buffer.add (mode_indent s len) tx,
150 ind = Buffer.add s ind,
161 fun make_margin_info m =
162 {margin = m, (*right margin, or page width*)
163 breakgain = m div 20, (*minimum added space required of a break*)
164 emergencypos = m div 2}; (*position too far to right*)
166 val margin_info = ref (make_margin_info 76);
167 fun setmargin m = margin_info := make_margin_info m;
168 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
173 (*Add the lengths of the expressions until the next Break; if no Break then
174 include "after", to account for text following this block.*)
175 fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
176 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
177 | breakdist (Break _ :: es, after) = 0
178 | breakdist ([], after) = after;
180 (*Search for the next break (at this or higher levels) and force it to occur.*)
181 fun forcenext [] = []
182 | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
183 | forcenext (e :: es) = e :: forcenext es;
185 (*es is list of expressions to print;
186 blockin is the indentation of the current block;
187 after is the width of the following context until next break.*)
188 fun format ([], _, _) text = text
189 | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
191 Block (markup, bes, indent, wd) =>
193 val {emergencypos, ...} = ! margin_info;
194 val pos' = pos + indent;
195 val pos'' = pos' mod emergencypos;
197 if pos' < emergencypos then (ind |> add_indent indent, pos')
198 else (set_indent pos'', pos'');
199 val (bg, en) = if markup = Markup.none then ("", "") else mode_markup markup;
200 val btext: text = text
202 |> format (bes, block', breakdist (es, after))
204 (*if this block was broken then force the next break*)
205 val es' = if nl < #nl btext then forcenext es else es;
206 in format (es', block, after) btext end
207 | String str => format (es, block, after) (string str text)
208 | Break (force, wd) =>
209 let val {margin, breakgain, ...} = ! margin_info in
210 (*no break if text to next break fits on this line
211 or if breaking would add only breakgain to space*)
212 format (es, block, after)
213 (if not force andalso
214 pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
215 then text |> blanks wd (*just insert wd blanks*)
216 else text |> newline |> indentation block)
220 (** Exported functions to create formatting expressions **)
222 fun length (Block (_, _, _, len)) = len
223 | length (String (_, len)) = len
224 | length (Break(_, wd)) = wd;
226 val raw_str = String;
227 val str = String o Output.output_width;
229 fun brk wd = Break (false, wd);
230 val fbrk = Break (true, 2);
232 fun markup_block m (indent, es) =
235 | sum (e :: es) k = sum es (length e + k);
236 in Block (m, es, indent, sum es 0) end;
238 val blk = markup_block Markup.none;
240 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
241 | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
242 | unbreakable (e as String _) = e;
247 fun breaks prts = Library.separate (brk 1) prts;
248 fun fbreaks prts = Library.separate fbrk prts;
250 fun block prts = blk (2, prts);
251 fun markup m prts = markup_block m (0, prts);
253 fun keyword name = markup (Markup.keyword name) [str name];
254 fun command name = markup (Markup.command name) [str name];
256 val strs = block o breaks o map str;
257 fun chunks prts = blk (0, fbreaks prts);
258 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
259 fun block_enclose (p1, p2) ps = chunks [(block o fbreaks) (p1 :: ps), p2];
261 fun quote prt = blk (1, [str "\"", prt, str "\""]);
262 fun backquote prt = blk (1, [str "`", prt, str "`"]);
264 fun separate sep prts =
265 flat (Library.separate [str sep, brk 1] (map single prts));
267 val commas = separate ",";
269 fun enclose lpar rpar prts =
270 block (str lpar :: (prts @ [str rpar]));
272 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
275 fun str_list lpar rpar strs = list lpar rpar (map str strs);
277 fun big_list name prts = block (fbreaks (str name :: prts));
279 fun indent 0 prt = prt
280 | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
284 (** Pretty printing with depth limitation **)
286 val depth = ref 0; (*maximum depth; 0 means no limit*)
288 fun setdepth dp = (depth := dp);
290 (*Recursively prune blocks, discarding all text exceeding depth dp*)
291 fun pruning dp (Block (m, bes, indent, wd)) =
293 then markup_block m (indent, map (pruning (dp - 1)) bes)
297 fun prune dp e = if dp > 0 then pruning dp e else e;
299 fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty);
300 val output = Buffer.content o output_buffer;
301 val string_of = Output.escape o output;
302 val writeln = Output.writeln o string_of;
305 (*Create a single flat string: no line breaking*)
308 fun fmt (Block (m, prts, _, _)) =
309 let val (bg, en) = mode_markup m
310 in Buffer.add bg #> fold fmt prts #> Buffer.add en end
311 | fmt (String (s, _)) = Buffer.add s
312 | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
313 | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
314 in Output.escape (Buffer.content (fmt (prune (! depth) prt) Buffer.empty)) end;
316 (*part of the interface to the ML toplevel pretty printers*)
317 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
319 fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
320 | pp (String (s, _)) = put_str s
321 | pp (Break (false, wd)) = put_brk wd
322 | pp (Break (true, _)) = put_fbrk ()
324 | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
325 in pp (prune (! depth) prt) end;
329 (** abstract pretty printing context **)
332 PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
336 fun pp_fun f (PP x) = f x;
338 val term = pp_fun #1;
340 val sort = pp_fun #3;
341 val classrel = pp_fun #4;
342 val arity = pp_fun #5;
344 val string_of_term = string_of oo term;
345 val string_of_typ = string_of oo typ;
346 val string_of_sort = string_of oo sort;
347 val string_of_classrel = string_of oo classrel;
348 val string_of_arity = string_of oo arity;