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 markup_chunks: Markup.T -> T list -> T
46 val chunks: T list -> T
47 val chunks2: T list -> T
48 val block_enclose: T * T -> T list -> T
51 val separate: string -> T list -> T list
52 val commas: T list -> T list
53 val enclose: string -> string -> T list -> T
54 val enum: string -> string -> string -> T list -> T
55 val list: string -> string -> T list -> T
56 val str_list: string -> string -> string list -> T
57 val big_list: string -> T list -> T
58 val indent: int -> T -> T
59 val string_of: T -> string
60 val output_buffer: T -> Buffer.T
61 val output: T -> string
62 val writeln: T -> unit
63 val str_of: T -> string
64 val pprint: T -> pprint_args -> unit
65 val setdepth: int -> unit
66 val setmargin: int -> unit
67 val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
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;
88 fun default_markup (_: Markup.T) = ("", "");
91 val default = {indent = default_indent, markup = default_markup};
92 val modes = ref (Symtab.make [("", default)]);
94 fun add_mode name indent markup =
95 change modes (Symtab.update_new (name, {indent = indent, markup = markup}));
97 the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
100 fun mode_indent x y = #indent (get_mode ()) x y;
101 fun mode_markup x = #markup (get_mode ()) x;
105 (** printing items: compound phrases, strings, and breaks **)
108 Block of Markup.T * T list * int * int | (*markup, body, indentation, length*)
109 String of string * int | (*text, length*)
110 Break of bool * int; (*mandatory flag, width if not taken*)
116 val output_spaces = Output.output o Symbol.spaces;
117 val add_indent = Buffer.add o output_spaces;
118 fun set_indent wd = Buffer.empty |> add_indent wd;
120 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
128 fun newline {tx, ind, pos, nl} : text =
129 {tx = Buffer.add (Output.output "\n") tx,
134 fun control s {tx, ind, pos: int, nl} : text =
135 {tx = Buffer.add s tx,
140 fun string (s, len) {tx, ind, pos: int, nl} : text =
141 {tx = Buffer.add s tx,
142 ind = Buffer.add s ind,
146 fun blanks wd = string (output_spaces wd, wd);
148 fun indentation (buf, len) {tx, ind, pos, nl} : text =
149 let val s = Buffer.content buf in
150 {tx = Buffer.add (mode_indent s len) tx,
151 ind = Buffer.add s ind,
162 fun make_margin_info m =
163 {margin = m, (*right margin, or page width*)
164 breakgain = m div 20, (*minimum added space required of a break*)
165 emergencypos = m div 2}; (*position too far to right*)
167 val margin_info = ref (make_margin_info 76);
168 fun setmargin m = margin_info := make_margin_info m;
169 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
174 (*Add the lengths of the expressions until the next Break; if no Break then
175 include "after", to account for text following this block.*)
176 fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
177 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
178 | breakdist (Break _ :: es, after) = 0
179 | breakdist ([], after) = after;
181 (*Search for the next break (at this or higher levels) and force it to occur.*)
182 fun forcenext [] = []
183 | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
184 | forcenext (e :: es) = e :: forcenext es;
186 (*es is list of expressions to print;
187 blockin is the indentation of the current block;
188 after is the width of the following context until next break.*)
189 fun format ([], _, _) text = text
190 | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
192 Block (markup, bes, indent, wd) =>
194 val {emergencypos, ...} = ! margin_info;
195 val pos' = pos + indent;
196 val pos'' = pos' mod emergencypos;
198 if pos' < emergencypos then (ind |> add_indent indent, pos')
199 else (set_indent pos'', pos'');
200 val (bg, en) = if markup = Markup.none then ("", "") else mode_markup markup;
201 val btext: text = text
203 |> format (bes, block', breakdist (es, after))
205 (*if this block was broken then force the next break*)
206 val es' = if nl < #nl btext then forcenext es else es;
207 in format (es', block, after) btext end
208 | String str => format (es, block, after) (string str text)
209 | Break (force, wd) =>
210 let val {margin, breakgain, ...} = ! margin_info in
211 (*no break if text to next break fits on this line
212 or if breaking would add only breakgain to space*)
213 format (es, block, after)
214 (if not force andalso
215 pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
216 then text |> blanks wd (*just insert wd blanks*)
217 else text |> newline |> indentation block)
221 (** Exported functions to create formatting expressions **)
223 fun length (Block (_, _, _, len)) = len
224 | length (String (_, len)) = len
225 | length (Break(_, wd)) = wd;
227 val raw_str = String;
228 val str = String o Output.output_width;
230 fun brk wd = Break (false, wd);
231 val fbrk = Break (true, 2);
233 fun markup_block m (indent, es) =
236 | sum (e :: es) k = sum es (length e + k);
237 in Block (m, es, indent, sum es 0) end;
239 val blk = markup_block Markup.none;
241 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
242 | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
243 | unbreakable (e as String _) = e;
248 fun breaks prts = Library.separate (brk 1) prts;
249 fun fbreaks prts = Library.separate fbrk prts;
251 fun block prts = blk (2, prts);
252 fun markup m prts = markup_block m (0, prts);
254 fun keyword name = markup (Markup.keyword name) [str name];
255 fun command name = markup (Markup.command name) [str name];
257 val strs = block o breaks o map str;
259 fun markup_chunks m prts = markup m (fbreaks prts);
260 val chunks = markup_chunks Markup.none;
262 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
263 fun block_enclose (p1, p2) ps = chunks [(block o fbreaks) (p1 :: ps), p2];
265 fun quote prt = blk (1, [str "\"", prt, str "\""]);
266 fun backquote prt = blk (1, [str "`", prt, str "`"]);
268 fun separate sep prts =
269 flat (Library.separate [str sep, brk 1] (map single prts));
271 val commas = separate ",";
273 fun enclose lpar rpar prts =
274 block (str lpar :: (prts @ [str rpar]));
276 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
279 fun str_list lpar rpar strs = list lpar rpar (map str strs);
281 fun big_list name prts = block (fbreaks (str name :: prts));
283 fun indent 0 prt = prt
284 | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
288 (** Pretty printing with depth limitation **)
290 val depth = ref 0; (*maximum depth; 0 means no limit*)
292 fun setdepth dp = (depth := dp);
294 (*Recursively prune blocks, discarding all text exceeding depth dp*)
295 fun pruning dp (Block (m, bes, indent, wd)) =
297 then markup_block m (indent, map (pruning (dp - 1)) bes)
301 fun prune dp e = if dp > 0 then pruning dp e else e;
303 fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty);
304 val output = Buffer.content o output_buffer;
305 val string_of = Output.escape o output;
306 val writeln = Output.writeln o string_of;
309 (*Create a single flat string: no line breaking*)
312 fun fmt (Block (m, prts, _, _)) =
313 let val (bg, en) = mode_markup m
314 in Buffer.add bg #> fold fmt prts #> Buffer.add en end
315 | fmt (String (s, _)) = Buffer.add s
316 | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
317 | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
318 in Output.escape (Buffer.content (fmt (prune (! depth) prt) Buffer.empty)) end;
320 (*part of the interface to the ML toplevel pretty printers*)
321 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
323 fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
324 | pp (String (s, _)) = put_str s
325 | pp (Break (false, wd)) = put_brk wd
326 | pp (Break (true, _)) = put_fbrk ()
328 | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
329 in pp (prune (! depth) prt) end;
333 (** abstract pretty printing context **)
336 PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
340 fun pp_fun f (PP x) = f x;
342 val term = pp_fun #1;
344 val sort = pp_fun #3;
345 val classrel = pp_fun #4;
346 val arity = pp_fun #5;
348 val string_of_term = string_of oo term;
349 val string_of_typ = string_of oo typ;
350 val string_of_sort = string_of oo sort;
351 val string_of_classrel = string_of oo classrel;
352 val string_of_arity = string_of oo arity;