1 (* Title: Pure/General/pretty.ML
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Author: Markus Wenzel, TU Munich
5 Generic pretty printing module.
8 D. C. Oppen, "Pretty Printing",
9 ACM Transactions on Programming Languages and Systems (1980), 465-483.
11 The object to be printed is given as a tree with indentation and line
12 breaking information. A "break" inserts a newline if the text until
13 the next break is too long to fit on the current line. After the newline,
14 text is indented to the level of the enclosing block. Normally, if a block
15 is broken then all enclosing blocks will also be broken. Only "inconsistent
18 The stored length of a block is used in breakdist (to treat each inner block as
24 val default_indent: string -> int -> Output.output
25 val add_mode: string -> (string -> int -> Output.output) -> unit
30 val breaks: T list -> T list
31 val fbreaks: T list -> T list
32 val blk: int * T list -> T
33 val block: T list -> T
34 val strs: string list -> T
35 val markup: Markup.T -> T list -> T
36 val mark: Markup.T -> T -> T
37 val mark_str: Markup.T * string -> T
38 val marks_str: Markup.T list * string -> T
39 val keyword: string -> T
40 val command: string -> T
41 val markup_chunks: Markup.T -> T list -> T
42 val chunks: T list -> T
43 val chunks2: T list -> T
44 val block_enclose: T * T -> T list -> T
47 val separate: string -> T list -> T list
48 val commas: T list -> T list
49 val enclose: string -> string -> T list -> T
50 val enum: string -> string -> string -> T list -> T
51 val position: Position.T -> T
52 val list: string -> string -> T list -> T
53 val str_list: string -> string -> string list -> T
54 val big_list: string -> T list -> T
55 val indent: int -> T -> T
56 val unbreakable: T -> T
57 val margin_default: int Unsynchronized.ref
59 val output_buffer: int option -> T -> Buffer.T
60 val output: int option -> T -> Output.output
61 val string_of_margin: int -> T -> string
62 val string_of: T -> string
63 val str_of: T -> string
64 val writeln: T -> unit
65 val to_ML: T -> ML_Pretty.pretty
66 val from_ML: ML_Pretty.pretty -> T
69 structure Pretty: PRETTY =
72 (** print mode operations **)
74 fun default_indent (_: string) = Symbol.spaces;
77 val default = {indent = default_indent};
78 val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
80 fun add_mode name indent =
81 Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
84 (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
87 fun mode_indent x y = #indent (get_mode ()) x y;
89 val output_spaces = Output.output o Symbol.spaces;
90 val add_indent = Buffer.add o output_spaces;
94 (** printing items: compound phrases, strings, and breaks **)
97 Block of (Output.output * Output.output) * T list * int * int
98 (*markup output, body, indentation, length*)
99 | String of Output.output * int (*text, length*)
100 | Break of bool * int (*mandatory flag, width if not taken*)
103 fun length (Block (_, _, _, len)) = len
104 | length (String (_, len)) = len
105 | length (Break (_, wd)) = wd;
109 (** derived operations to create formatting expressions **)
111 val str = String o Output.output_width;
113 fun brk wd = Break (false, wd);
114 val fbrk = Break (true, 1);
116 fun breaks prts = Library.separate (brk 1) prts;
117 fun fbreaks prts = Library.separate fbrk prts;
119 fun block_markup m (indent, es) =
122 | sum (e :: es) k = sum es (length e + k);
123 in Block (m, es, indent, sum es 0) end;
125 fun markup_block m arg = block_markup (Markup.output m) arg;
127 val blk = markup_block Markup.empty;
128 fun block prts = blk (2, prts);
129 val strs = block o breaks o map str;
131 fun markup m prts = markup_block m (0, prts);
132 fun mark m prt = if m = Markup.empty then prt else markup m [prt];
133 fun mark_str (m, s) = mark m (str s);
134 fun marks_str (ms, s) = fold_rev mark ms (str s);
136 fun keyword name = mark_str (Markup.keyword, name);
137 fun command name = mark_str (Markup.command, name);
139 fun markup_chunks m prts = markup m (fbreaks prts);
140 val chunks = markup_chunks Markup.empty;
141 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
143 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
145 fun quote prt = blk (1, [str "\"", prt, str "\""]);
146 fun backquote prt = blk (1, [str "`", prt, str "`"]);
148 fun separate sep prts =
149 flat (Library.separate [str sep, brk 1] (map single prts));
151 val commas = separate ",";
153 fun enclose lpar rpar prts =
154 block (str lpar :: (prts @ [str rpar]));
156 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
159 enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
162 fun str_list lpar rpar strs = list lpar rpar (map str strs);
164 fun big_list name prts = block (fbreaks (str name :: prts));
166 fun indent 0 prt = prt
167 | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
169 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
170 | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
171 | unbreakable (e as String _) = e;
177 (* formatted output *)
181 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
189 fun newline {tx, ind = _, pos = _, nl} : text =
190 {tx = Buffer.add (Output.output "\n") tx,
195 fun control s {tx, ind, pos: int, nl} : text =
196 {tx = Buffer.add s tx,
201 fun string (s, len) {tx, ind, pos: int, nl} : text =
202 {tx = Buffer.add s tx,
203 ind = Buffer.add s ind,
207 fun blanks wd = string (output_spaces wd, wd);
209 fun indentation (buf, len) {tx, ind, pos, nl} : text =
210 let val s = Buffer.content buf in
211 {tx = Buffer.add (mode_indent s len) tx,
212 ind = Buffer.add s ind,
217 (*Add the lengths of the expressions until the next Break; if no Break then
218 include "after", to account for text following this block.*)
219 fun breakdist (Break _ :: _, _) = 0
220 | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
221 | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
222 | breakdist ([], after) = after;
224 (*Search for the next break (at this or higher levels) and force it to occur.*)
225 fun forcenext [] = []
226 | forcenext (Break _ :: es) = fbrk :: es
227 | forcenext (e :: es) = e :: forcenext es;
231 fun formatted margin input =
233 val breakgain = margin div 20; (*minimum added space required of a break*)
234 val emergencypos = margin div 2; (*position too far to right*)
236 (*es is list of expressions to print;
237 blockin is the indentation of the current block;
238 after is the width of the following context until next break.*)
239 fun format ([], _, _) text = text
240 | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
242 Block ((bg, en), bes, indent, _) =>
244 val pos' = pos + indent;
245 val pos'' = pos' mod emergencypos;
247 if pos' < emergencypos then (ind |> add_indent indent, pos')
248 else (add_indent pos'' Buffer.empty, pos'');
249 val btext: text = text
251 |> format (bes, block', breakdist (es, after))
253 (*if this block was broken then force the next break*)
254 val es' = if nl < #nl btext then forcenext es else es;
255 in format (es', block, after) btext end
256 | Break (force, wd) =>
257 (*no break if text to next break fits on this line
258 or if breaking would add only breakgain to space*)
259 format (es, block, after)
260 (if not force andalso
261 pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
262 then text |> blanks wd (*just insert wd blanks*)
263 else text |> newline |> indentation block)
264 | String str => format (es, block, after) (string str text));
266 #tx (format ([input], (Buffer.empty, 0), 0) empty)
274 (*symbolic markup -- no formatting*)
277 fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
278 | out (Block ((bg, en), prts, indent, _)) =
279 Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
280 | out (String (s, _)) = Buffer.add s
281 | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
282 | out (Break (true, _)) = Buffer.add (Output.output "\n");
283 in out prt Buffer.empty end;
285 (*unformatted output*)
286 fun unformatted prt =
288 fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
289 | fmt (String (s, _)) = Buffer.add s
290 | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
291 in fmt prt Buffer.empty end;
294 (* output interfaces *)
296 val margin_default = Unsynchronized.ref 76; (*right margin, or page width*)
298 val symbolicN = "pretty_symbolic";
300 fun output_buffer margin prt =
301 if print_mode_active symbolicN then symbolic prt
302 else formatted (the_default (! margin_default) margin) prt;
304 val output = Buffer.content oo output_buffer;
305 fun string_of_margin margin = Output.escape o output (SOME margin);
306 val string_of = Output.escape o output NONE;
307 val str_of = Output.escape o Buffer.content o unformatted;
308 val writeln = Output.writeln o string_of;
312 (** ML toplevel pretty printing **)
314 fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
315 | to_ML (String s) = ML_Pretty.String s
316 | to_ML (Break b) = ML_Pretty.Break b;
318 fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
319 | from_ML (ML_Pretty.String s) = String s
320 | from_ML (ML_Pretty.Break b) = Break b;