|
1 (* Title: Pure/Syntax/pretty.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Generic pretty printing module. |
|
7 |
|
8 Loosely based on |
|
9 D. C. Oppen, "Pretty Printing", |
|
10 ACM Transactions on Programming Languages and Systems (1980), 465-483. |
|
11 |
|
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 |
|
17 breaks" are provided. |
|
18 |
|
19 The stored length of a block is used in breakdist (to treat each inner block as |
|
20 a unit for breaking). |
|
21 *) |
|
22 |
|
23 type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) * |
|
24 (unit -> unit) * (unit -> unit); |
|
25 |
|
26 signature PRETTY = |
|
27 sig |
|
28 type T |
|
29 val str: string -> T |
|
30 val strlen: string -> int -> T |
|
31 val sym: string -> T |
|
32 val spc: int -> T |
|
33 val brk: int -> T |
|
34 val fbrk: T |
|
35 val blk: int * T list -> T |
|
36 val lst: string * string -> T list -> T |
|
37 val quote: T -> T |
|
38 val commas: T list -> T list |
|
39 val breaks: T list -> T list |
|
40 val fbreaks: T list -> T list |
|
41 val block: T list -> T |
|
42 val strs: string list -> T |
|
43 val enclose: string -> string -> T list -> T |
|
44 val list: string -> string -> T list -> T |
|
45 val str_list: string -> string -> string list -> T |
|
46 val big_list: string -> T list -> T |
|
47 val string_of: T -> string |
|
48 val writeln: T -> unit |
|
49 val str_of: T -> string |
|
50 val pprint: T -> pprint_args -> unit |
|
51 val setdepth: int -> unit |
|
52 val setmargin: int -> unit |
|
53 end; |
|
54 |
|
55 structure Pretty : PRETTY = |
|
56 struct |
|
57 |
|
58 (*printing items: compound phrases, strings, and breaks*) |
|
59 datatype T = |
|
60 Block of T list * int * int | (*body, indentation, length*) |
|
61 String of string * int | (*text, length*) |
|
62 Break of bool * int; (*mandatory flag, width if not taken*); |
|
63 |
|
64 (*Add the lengths of the expressions until the next Break; if no Break then |
|
65 include "after", to account for text following this block. *) |
|
66 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after) |
|
67 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after) |
|
68 | breakdist (Break _ :: es, after) = 0 |
|
69 | breakdist ([], after) = after; |
|
70 |
|
71 fun repstring a 0 = "" |
|
72 | repstring a 1 = a |
|
73 | repstring a k = |
|
74 if k mod 2 = 0 then repstring(a^a) (k div 2) |
|
75 else repstring(a^a) (k div 2) ^ a; |
|
76 |
|
77 (*** Type for lines of text: string, # of lines, position on line ***) |
|
78 |
|
79 type text = {tx: string, nl: int, pos: int}; |
|
80 |
|
81 val emptytext = {tx="", nl=0, pos=0}; |
|
82 |
|
83 fun blanks wd {tx,nl,pos} = |
|
84 {tx = tx ^ repstring " " wd, |
|
85 nl = nl, |
|
86 pos = pos+wd}; |
|
87 |
|
88 fun newline {tx,nl,pos} = |
|
89 {tx = tx ^ "\n", |
|
90 nl = nl+1, |
|
91 pos = 0}; |
|
92 |
|
93 fun string s len {tx,nl,pos:int} = |
|
94 {tx = tx ^ s, |
|
95 nl = nl, |
|
96 pos = pos + len}; |
|
97 |
|
98 |
|
99 (*** Formatting ***) |
|
100 |
|
101 (* margin *) |
|
102 |
|
103 (*example values*) |
|
104 val margin = ref 80 (*right margin, or page width*) |
|
105 and breakgain = ref 4 (*minimum added space required of a break*) |
|
106 and emergencypos = ref 40; (*position too far to right*) |
|
107 |
|
108 fun setmargin m = |
|
109 (margin := m; |
|
110 breakgain := !margin div 20; |
|
111 emergencypos := !margin div 2); |
|
112 |
|
113 val () = setmargin 76; |
|
114 |
|
115 |
|
116 (*Search for the next break (at this or higher levels) and force it to occur*) |
|
117 fun forcenext [] = [] |
|
118 | forcenext (Break(_,wd) :: es) = Break(true,0) :: es |
|
119 | forcenext (e :: es) = e :: forcenext es; |
|
120 |
|
121 (*es is list of expressions to print; |
|
122 blockin is the indentation of the current block; |
|
123 after is the width of the following context until next break. *) |
|
124 fun format ([], _, _) text = text |
|
125 | format (e::es, blockin, after) (text as {pos,nl,...}) = |
|
126 (case e of |
|
127 Block(bes,indent,wd) => |
|
128 let val blockin' = (pos + indent) mod !emergencypos |
|
129 val btext = format(bes, blockin', breakdist(es,after)) text |
|
130 (*If this block was broken then force the next break.*) |
|
131 val es2 = if nl < #nl(btext) then forcenext es else es |
|
132 in format (es2,blockin,after) btext end |
|
133 | String (s, len) => format (es,blockin,after) (string s len text) |
|
134 | Break(force,wd) => (*no break if text to next break fits on this line |
|
135 or if breaking would add only breakgain to space *) |
|
136 format (es,blockin,after) |
|
137 (if not force andalso |
|
138 pos+wd <= Int.max(!margin - breakdist(es,after), |
|
139 blockin + !breakgain) |
|
140 then blanks wd text (*just insert wd blanks*) |
|
141 else blanks blockin (newline text))); |
|
142 |
|
143 |
|
144 (*** Exported functions to create formatting expressions ***) |
|
145 |
|
146 fun length (Block (_, _, len)) = len |
|
147 | length (String (_, len)) = len |
|
148 | length (Break(_, wd)) = wd; |
|
149 |
|
150 fun str s = String (s, size s); |
|
151 fun strlen s len = String (s, len); |
|
152 fun sym s = String (s, Symbol.size s); |
|
153 |
|
154 fun spc n = str (repstring " " n); |
|
155 |
|
156 fun brk wd = Break (false, wd); |
|
157 val fbrk = Break (true, 0); |
|
158 |
|
159 fun blk (indent, es) = |
|
160 let |
|
161 fun sum([], k) = k |
|
162 | sum(e :: es, k) = sum (es, length e + k); |
|
163 in Block (es, indent, sum (es, 0)) end; |
|
164 |
|
165 (*Join the elements of es as a comma-separated list, bracketted by lp and rp*) |
|
166 fun lst(lp,rp) es = |
|
167 let fun add(e,es) = str"," :: brk 1 :: e :: es; |
|
168 fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp]) |
|
169 | list(e::[]) = [str lp, e, str rp] |
|
170 | list([]) = [] |
|
171 in blk(size lp, list es) end; |
|
172 |
|
173 |
|
174 (* utils *) |
|
175 |
|
176 fun quote prt = |
|
177 blk (1, [str "\"", prt, str "\""]); |
|
178 |
|
179 fun commas prts = |
|
180 flat (separate [str ",", brk 1] (map (fn x => [x]) prts)); |
|
181 |
|
182 fun breaks prts = separate (brk 1) prts; |
|
183 |
|
184 fun fbreaks prts = separate fbrk prts; |
|
185 |
|
186 fun block prts = blk (2, prts); |
|
187 |
|
188 val strs = block o breaks o (map str); |
|
189 |
|
190 fun enclose lpar rpar prts = |
|
191 block (str lpar :: (prts @ [str rpar])); |
|
192 |
|
193 fun list lpar rpar prts = |
|
194 enclose lpar rpar (commas prts); |
|
195 |
|
196 fun str_list lpar rpar strs = |
|
197 list lpar rpar (map str strs); |
|
198 |
|
199 fun big_list name prts = |
|
200 block (fbreaks (str name :: prts)); |
|
201 |
|
202 |
|
203 |
|
204 (*** Pretty printing with depth limitation ***) |
|
205 |
|
206 val depth = ref 0; (*maximum depth; 0 means no limit*) |
|
207 |
|
208 fun setdepth dp = (depth := dp); |
|
209 |
|
210 (*Recursively prune blocks, discarding all text exceeding depth dp*) |
|
211 fun pruning dp (Block(bes,indent,wd)) = |
|
212 if dp>0 then blk(indent, map (pruning(dp-1)) bes) |
|
213 else str "..." |
|
214 | pruning dp e = e; |
|
215 |
|
216 fun prune dp e = if dp>0 then pruning dp e else e; |
|
217 |
|
218 |
|
219 fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext); |
|
220 |
|
221 val writeln = writeln o string_of; |
|
222 |
|
223 |
|
224 (*Create a single flat string: no line breaking*) |
|
225 fun str_of prt = |
|
226 let |
|
227 fun s_of (Block (prts, _, _)) = implode (map s_of prts) |
|
228 | s_of (String (s, _)) = s |
|
229 | s_of (Break (false, wd)) = repstring " " wd |
|
230 | s_of (Break (true, _)) = " "; |
|
231 in |
|
232 s_of (prune (! depth) prt) |
|
233 end; |
|
234 |
|
235 (*Part of the interface to the Poly/ML and New Jersey ML pretty printers*) |
|
236 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) = |
|
237 let |
|
238 fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ()) |
|
239 | pp (String (s, _)) = put_str s |
|
240 | pp (Break (false, wd)) = put_brk wd |
|
241 | pp (Break (true, _)) = put_fbrk () |
|
242 and pp_lst [] = () |
|
243 | pp_lst (prt :: prts) = (pp prt; pp_lst prts); |
|
244 in |
|
245 pp (prune (! depth) prt) |
|
246 end; |
|
247 |
|
248 |
|
249 end; |