1 (* Title: Pure/General/pretty.ML
3 Author: Lawrence C Paulson
4 Copyright 1991 University of Cambridge
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);
29 val raw_str: string * real -> T
33 val blk: int * T list -> T
35 val commas: T list -> T list
36 val breaks: T list -> T list
37 val fbreaks: T list -> T list
38 val block: T list -> T
39 val strs: string list -> T
40 val enclose: string -> string -> T list -> T
41 val list: string -> string -> T list -> T
42 val str_list: string -> string -> string list -> T
43 val big_list: string -> T list -> T
44 val chunks: T list -> T
45 val string_of: T -> string
46 val writeln: T -> unit
47 val str_of: T -> string
48 val pprint: T -> pprint_args -> unit
49 val setdepth: int -> unit
50 val setmargin: int -> unit
51 val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
54 structure Pretty : PRETTY =
57 (*printing items: compound phrases, strings, and breaks*)
59 Block of T list * int * int | (*body, indentation, length*)
60 String of string * int | (*text, length*)
61 Break of bool * int; (*mandatory flag, width if not taken*);
63 (*Add the lengths of the expressions until the next Break; if no Break then
64 include "after", to account for text following this block. *)
65 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
66 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
67 | breakdist (Break _ :: es, after) = 0
68 | breakdist ([], after) = after;
70 fun repstring a 0 = ""
73 if k mod 2 = 0 then repstring(a^a) (k div 2)
74 else repstring(a^a) (k div 2) ^ a;
76 (*** Type for lines of text: string, # of lines, position on line ***)
78 type text = {tx: Buffer.T, nl: int, pos: int};
80 val emptytext = {tx = Buffer.empty, nl = 0, pos = 0};
82 fun blanks wd {tx, nl, pos} =
83 {tx = Buffer.add (Symbol.output (repstring " " wd)) tx,
87 fun newline {tx, nl, pos} =
88 {tx = Buffer.add (Symbol.output "\n") tx,
92 fun string s len {tx, nl, pos:int} =
93 {tx = Buffer.add s tx,
102 fun make_margin_info m =
103 {margin = m, (*right margin, or page width*)
104 breakgain = m div 20, (*minimum added space required of a break*)
105 emergencypos = m div 2}; (*position too far to right*)
107 val margin_info = ref (make_margin_info 76);
108 fun setmargin m = margin_info := make_margin_info m;
109 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
111 (*Search for the next break (at this or higher levels) and force it to occur*)
112 fun forcenext [] = []
113 | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
114 | forcenext (e :: es) = e :: forcenext es;
116 (*es is list of expressions to print;
117 blockin is the indentation of the current block;
118 after is the width of the following context until next break. *)
119 fun format ([], _, _) text = text
120 | format (e::es, blockin, after) (text as {pos,nl,...}) =
122 Block(bes,indent,wd) =>
123 let val blockin' = (pos + indent) mod #emergencypos (! margin_info)
124 val btext = format(bes, blockin', breakdist(es,after)) text
125 (*If this block was broken then force the next break.*)
126 val es2 = if nl < #nl(btext) then forcenext es else es
127 in format (es2,blockin,after) btext end
128 | String (s, len) => format (es,blockin,after) (string s len text)
129 | Break(force,wd) => (*no break if text to next break fits on this line
130 or if breaking would add only breakgain to space *)
131 format (es,blockin,after)
132 (if not force andalso
133 pos+wd <= Int.max(#margin (! margin_info) - breakdist(es,after),
134 blockin + #breakgain (! margin_info))
135 then blanks wd text (*just insert wd blanks*)
136 else blanks blockin (newline text)));
139 (*** Exported functions to create formatting expressions ***)
141 fun length (Block (_, _, len)) = len
142 | length (String (_, len)) = len
143 | length (Break(_, wd)) = wd;
145 fun raw_str (s, len) = String (s, Real.round len);
146 val str = String o apsnd Real.round o Symbol.output_width;
148 fun brk wd = Break (false, wd);
149 val fbrk = Break (true, 0);
151 fun blk (indent, es) =
154 | sum(e :: es, k) = sum (es, length e + k);
155 in Block (es, indent, sum (es, 0)) end;
161 blk (1, [str "\"", prt, str "\""]);
164 flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
166 fun breaks prts = separate (brk 1) prts;
167 fun fbreaks prts = separate fbrk prts;
169 fun block prts = blk (2, prts);
171 val strs = block o breaks o (map str);
173 fun enclose lpar rpar prts =
174 block (str lpar :: (prts @ [str rpar]));
176 fun list lpar rpar prts = enclose lpar rpar (commas prts);
177 fun str_list lpar rpar strs = list lpar rpar (map str strs);
178 fun big_list name prts = block (fbreaks (str name :: prts));
179 fun chunks prts = blk (0, fbreaks prts);
182 (*** Pretty printing with depth limitation ***)
184 val depth = ref 0; (*maximum depth; 0 means no limit*)
186 fun setdepth dp = (depth := dp);
188 (*Recursively prune blocks, discarding all text exceeding depth dp*)
189 fun pruning dp (Block(bes,indent,wd)) =
190 if dp>0 then blk(indent, map (pruning(dp-1)) bes)
194 fun prune dp e = if dp>0 then pruning dp e else e;
197 fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], 0, 0) emptytext));
199 val writeln = writeln o string_of;
202 (*Create a single flat string: no line breaking*)
205 fun s_of (Block (prts, _, _)) = implode (map s_of prts)
206 | s_of (String (s, _)) = s
207 | s_of (Break (false, wd)) = Symbol.output (repstring " " wd)
208 | s_of (Break (true, _)) = Symbol.output " ";
209 in s_of (prune (! depth) prt) end;
211 (*part of the interface to the ML toplevel pretty printers*)
212 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
214 fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
215 | pp (String (s, _)) = put_str s
216 | pp (Break (false, wd)) = put_brk wd
217 | pp (Break (true, _)) = put_fbrk ()
219 | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
221 pp (prune (! depth) prt)