43 val big_list: string -> T list -> T |
44 val big_list: string -> T list -> T |
44 val string_of: T -> string |
45 val string_of: T -> string |
45 val writeln: T -> unit |
46 val writeln: T -> unit |
46 val str_of: T -> string |
47 val str_of: T -> string |
47 val pprint: T -> pprint_args -> unit |
48 val pprint: T -> pprint_args -> unit |
48 val map_strs: (string -> string) -> T -> T |
|
49 val setdepth: int -> unit |
49 val setdepth: int -> unit |
50 val setmargin: int -> unit |
50 val setmargin: int -> unit |
51 end; |
51 end; |
52 |
52 |
53 structure Pretty : PRETTY = |
53 structure Pretty : PRETTY = |
54 struct |
54 struct |
55 |
55 |
56 (*Printing items: compound phrases, strings, and breaks*) |
56 (*printing items: compound phrases, strings, and breaks*) |
57 datatype T = Block of T list * int * int (*indentation, length*) |
57 datatype T = |
58 | String of string |
58 Block of T list * int * int | (*body, indentation, length*) |
59 | Break of bool*int (*mandatory flag; width if not taken*); |
59 String of string * int | (*text, length*) |
|
60 Break of bool * int; (*mandatory flag, width if not taken*); |
60 |
61 |
61 (*Add the lengths of the expressions until the next Break; if no Break then |
62 (*Add the lengths of the expressions until the next Break; if no Break then |
62 include "after", to account for text following this block. *) |
63 include "after", to account for text following this block. *) |
63 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after) |
64 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after) |
64 | breakdist (String s :: es, after) = size s + breakdist (es, after) |
65 | breakdist (String (s, len) :: es, after) = len + breakdist (es, after) |
65 | breakdist (Break _ :: es, after) = 0 |
66 | breakdist (Break _ :: es, after) = 0 |
66 | breakdist ([], after) = after; |
67 | breakdist ([], after) = after; |
67 |
68 |
68 fun repstring a 0 = "" |
69 fun repstring a 0 = "" |
69 | repstring a 1 = a |
70 | repstring a 1 = a |
118 let val blockin' = (pos + indent) mod !emergencypos |
120 let val blockin' = (pos + indent) mod !emergencypos |
119 val btext = format(bes, blockin', breakdist(es,after)) text |
121 val btext = format(bes, blockin', breakdist(es,after)) text |
120 (*If this block was broken then force the next break.*) |
122 (*If this block was broken then force the next break.*) |
121 val es2 = if nl < #nl(btext) then forcenext es else es |
123 val es2 = if nl < #nl(btext) then forcenext es else es |
122 in format (es2,blockin,after) btext end |
124 in format (es2,blockin,after) btext end |
123 | String s => format (es,blockin,after) (string s text) |
125 | String (s, len) => format (es,blockin,after) (string s len text) |
124 | Break(force,wd) => (*no break if text to next break fits on this line |
126 | Break(force,wd) => (*no break if text to next break fits on this line |
125 or if breaking would add only breakgain to space *) |
127 or if breaking would add only breakgain to space *) |
126 format (es,blockin,after) |
128 format (es,blockin,after) |
127 (if not force andalso |
129 (if not force andalso |
128 pos+wd <= Int.max(!margin - breakdist(es,after), |
130 pos+wd <= Int.max(!margin - breakdist(es,after), |
129 blockin + !breakgain) |
131 blockin + !breakgain) |
130 then blanks wd text (*just insert wd blanks*) |
132 then blanks wd text (*just insert wd blanks*) |
131 else blanks blockin (newline text))); |
133 else blanks blockin (newline text))); |
132 |
134 |
|
135 |
133 (*** Exported functions to create formatting expressions ***) |
136 (*** Exported functions to create formatting expressions ***) |
134 |
137 |
135 fun length (Block(_,_,len)) = len |
138 fun length (Block (_, _, len)) = len |
136 | length (String s) = size s |
139 | length (String (_, len)) = len |
137 | length (Break(_,wd)) = wd; |
140 | length (Break(_, wd)) = wd; |
138 |
141 |
139 val str = String |
142 fun str s = String (s, size s); |
140 and fbrk = Break(true,0); |
143 fun strlen s len = String (s, len); |
141 |
144 |
142 fun brk wd = Break(false,wd); |
145 fun brk wd = Break (false, wd); |
143 |
146 val fbrk = Break (true, 0); |
144 fun blk (indent,es) = |
147 |
145 let fun sum([], k) = k |
148 fun blk (indent, es) = |
146 | sum(e::es, k) = sum(es, length e + k) |
149 let |
147 in Block(es,indent, sum(es,0)) end; |
150 fun sum([], k) = k |
|
151 | sum(e :: es, k) = sum (es, length e + k); |
|
152 in Block (es, indent, sum (es, 0)) end; |
148 |
153 |
149 (*Join the elements of es as a comma-separated list, bracketted by lp and rp*) |
154 (*Join the elements of es as a comma-separated list, bracketted by lp and rp*) |
150 fun lst(lp,rp) es = |
155 fun lst(lp,rp) es = |
151 let fun add(e,es) = str"," :: brk 1 :: e :: es; |
156 let fun add(e,es) = str"," :: brk 1 :: e :: es; |
152 fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp]) |
157 fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp]) |
207 |
212 |
208 (*Create a single flat string: no line breaking*) |
213 (*Create a single flat string: no line breaking*) |
209 fun str_of prt = |
214 fun str_of prt = |
210 let |
215 let |
211 fun s_of (Block (prts, _, _)) = implode (map s_of prts) |
216 fun s_of (Block (prts, _, _)) = implode (map s_of prts) |
212 | s_of (String s) = s |
217 | s_of (String (s, _)) = s |
213 | s_of (Break (false, wd)) = repstring " " wd |
218 | s_of (Break (false, wd)) = repstring " " wd |
214 | s_of (Break (true, _)) = " "; |
219 | s_of (Break (true, _)) = " "; |
215 in |
220 in |
216 s_of (prune (! depth) prt) |
221 s_of (prune (! depth) prt) |
217 end; |
222 end; |
218 |
223 |
219 (*Part of the interface to the Poly/ML and New Jersey ML pretty printers*) |
224 (*Part of the interface to the Poly/ML and New Jersey ML pretty printers*) |
220 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) = |
225 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) = |
221 let |
226 let |
222 fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ()) |
227 fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ()) |
223 | pp (String s) = put_str s |
228 | pp (String (s, _)) = put_str s |
224 | pp (Break (false, wd)) = put_brk wd |
229 | pp (Break (false, wd)) = put_brk wd |
225 | pp (Break (true, _)) = put_fbrk () |
230 | pp (Break (true, _)) = put_fbrk () |
226 and pp_lst [] = () |
231 and pp_lst [] = () |
227 | pp_lst (prt :: prts) = (pp prt; pp_lst prts); |
232 | pp_lst (prt :: prts) = (pp prt; pp_lst prts); |
228 in |
233 in |
229 pp (prune (! depth) prt) |
234 pp (prune (! depth) prt) |
230 end; |
235 end; |
231 |
236 |
232 (*Map strings*) |
|
233 fun map_strs f (Block (prts, ind, _)) = blk (ind, map (map_strs f) prts) |
|
234 | map_strs f (String s) = String (f s) |
|
235 | map_strs _ brk = brk; |
|
236 |
|
237 |
237 |
238 (*** Initialization ***) |
238 (*** Initialization ***) |
239 |
239 |
240 val () = setmargin 80; |
240 val () = setmargin 80; |
241 |
241 |
242 end; |
242 end; |
243 |
|