Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/src/comp-lib/pp.sml
ViewVC logotype

Annotation of /sml/trunk/src/comp-lib/pp.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 419 - (view) (download)

1 : monnier 245 (* pp.sml *)
2 :     (* Konrad Slind, <Konrad.Slind@cl.cam.ac.uk>, 5 May 1997 *)
3 :    
4 :     (*---------------------------------------------------------------------------
5 :     This defines an abstract type (ppstream) and associated operations. A
6 :     ppstream is an outstream that contains prettyprinting commands. The
7 :     commands are placed in the stream by various function calls listed below.
8 :     Periodically, an (mostly) invisible process goes through the stream
9 :     executing commands in the order in which they were added to the stream.
10 :    
11 :     One obtains a ppstream by "mk_ppstream". Its arguments are "linewidth"
12 :     (the maximum width in characters of the prettyprinted output) and
13 :     "consumer" (the function that writes strings to the display).
14 :     One can get these parameters from a ppstream by "dest_ppstream".
15 :    
16 :     Then there are the usual Oppen primitives for adding commands into the
17 :     stream: begin_block, end_block, add_string, add_break, and add_newline.
18 :    
19 :     There are two operations on the stream. "clear_ppstream" is used
20 :     to restart a given stream, while keeping everything else about the stream
21 :     intact. An example of its use is when an error occurs during
22 :     prettyprinting; in that case the top level printing function can catch
23 :     the exception and clear the ppstream. "flush_ppstream" is used at the
24 :     end of inserting commands, to order the invisible process to execute all
25 :     remaining commands in the stream. The last thing that flush_ppstream does
26 :     is call clear_ppstream.
27 :    
28 :     There is also an operation that hides the state-based implementation of
29 :     ppstream: "with_pp" takes a function operating on a ppstream, makes an
30 :     appropriate ppstream and applies the function to it, then flushes the
31 :     pp_stream and returns the value of the function. The ppstream is thus
32 :     only a local entity and is left to be garbage collected.
33 :    
34 :     CHANGE: May 4, 1997.
35 :    
36 :     Added two new internal fields to the ppstream datatype: "panic_column"
37 :     and "reset_column". When a block is "begun" at or past the panic
38 :     column, the block will instead begin at the reset column. This will
39 :     help control "runaway" prettyprinting. Currently, the panic column is
40 :     at 2/3 of the linewidth, and the reset column is at 1/3 the linewidth.
41 :    
42 :    
43 :     ---------------------------------------------------------------------------*)
44 :    
45 :     signature PRETTYPRINT =
46 :     sig
47 :     type ppstream
48 :     type ppconsumer (* = {consumer : string -> unit,
49 :     linewidth : int,
50 :     flush : unit -> unit} *)
51 :     datatype break_style
52 :     = CONSISTENT
53 :     | INCONSISTENT
54 :    
55 :     exception PP_FAIL of string
56 :    
57 :     val mk_ppstream : ppconsumer -> ppstream
58 :     val dest_ppstream : ppstream -> ppconsumer
59 :     val add_break : ppstream -> int * int -> unit
60 :     val add_newline : ppstream -> unit
61 :     val add_string : ppstream -> string -> unit
62 :     val begin_block : ppstream -> break_style -> int -> unit
63 :     val end_block : ppstream -> unit
64 :     val clear_ppstream : ppstream -> unit
65 :     val flush_ppstream : ppstream -> unit
66 :     val with_pp : ppconsumer -> (ppstream -> unit) -> unit
67 :     val pp_to_string : int -> (ppstream -> 'a -> unit) -> 'a -> string
68 :     end
69 :    
70 :    
71 :     structure PrettyPrint : PRETTYPRINT =
72 :     struct
73 :    
74 :     open Array infix 9 sub
75 :     open PPQueue
76 :    
77 :     exception PP_FAIL of string
78 :    
79 :     fun error msg = raise PP_FAIL ("PP FAILURE: " ^ msg)
80 :    
81 :     fun inc r = (r := !r + 1);
82 :     fun dec r = (r := !r - 1);
83 :    
84 :     datatype break_style = CONSISTENT | INCONSISTENT
85 :    
86 :     datatype break_info
87 :     = FITS
88 :     | PACK_ONTO_LINE of int
89 :     | ONE_PER_LINE of int
90 :    
91 :     (* Some global values *)
92 :     val INFINITY = 999999
93 :    
94 :     abstype indent_stack = Istack of break_info list ref
95 :     with
96 :     fun mk_indent_stack() = Istack (ref([]:break_info list))
97 :     fun clear_indent_stack (Istack stk) = (stk := ([]:break_info list))
98 :     fun top (Istack stk) =
99 :     case !stk
100 :     of nil => error "top: badly formed block"
101 :     | x::_ => x
102 :     fun push (x,(Istack stk)) = stk := x::(!stk)
103 :     fun pop (Istack stk) =
104 :     case !stk
105 :     of nil => error "pop: badly formed block"
106 :     | _::rest => stk := rest
107 :     end
108 :    
109 :     (*---------------------------------------------------------------------------
110 :     The delim_stack is used to compute the size of blocks. It is
111 :     a stack of indices into the token buffer. The indices only point to
112 :     BBs, Es, and BRs. We push BBs and Es onto the stack until a BR
113 :     is encountered. Then we compute sizes and pop. When we encounter
114 :     a BR in the middle of a block, we compute the Distance_to_next_break
115 :     of the previous BR in the block, if there was one.
116 :    
117 :     We need to be able to delete from the bottom of the delim_stack, so
118 :     we use a queue, treated with a stack discipline, i.e., we only add
119 :     items at the head of the queue, but can delete from the front or
120 :     back of the queue.
121 :     ---------------------------------------------------------------------------*)
122 :     abstype delim_stack = Dstack of int queue
123 :     with
124 :     fun new_delim_stack i = Dstack(mk_queue i ~1)
125 :     fun reset_delim_stack (Dstack q) = clear_queue q
126 :    
127 :     fun pop_delim_stack (Dstack d) = de_queue Qfront d
128 :     fun pop_bottom_delim_stack (Dstack d) = de_queue Qback d
129 :    
130 :     fun push_delim_stack(i,Dstack d) = en_queue Qfront i d
131 :     fun top_delim_stack (Dstack d) = queue_at Qfront d
132 :     fun bottom_delim_stack (Dstack d) = queue_at Qback d
133 :     fun delim_stack_is_empty (Dstack d) = is_empty d
134 :     end
135 :    
136 :    
137 :     type block_info = { Block_size : int ref,
138 :     Block_offset : int,
139 :     How_to_indent : break_style }
140 :    
141 :    
142 :     (*---------------------------------------------------------------------------
143 :     Distance_to_next_break includes Number_of_blanks. Break_offset is
144 :     a local offset for the break. BB represents a sequence of contiguous
145 :     Begins. E represents a sequence of contiguous Ends.
146 :     ---------------------------------------------------------------------------*)
147 :     datatype pp_token
148 :     = S of {String : string, Length : int}
149 :     | BB of {Pblocks : block_info list ref, (* Processed *)
150 :     Ublocks : block_info list ref} (* Unprocessed *)
151 :     | E of {Pend : int ref, Uend : int ref}
152 :     | BR of {Distance_to_next_break : int ref,
153 :     Number_of_blanks : int,
154 :     Break_offset : int}
155 :    
156 :    
157 :     (*---------------------------------------------------------------------------
158 :     The initial values in the token buffer
159 :     ----------------------------------------------------------------------------*)
160 :     val initial_token_value = S{String = "", Length = 0}
161 :    
162 :     datatype ppstream =
163 :     PPS of
164 :     {consumer : string -> unit,
165 :     linewidth : int,
166 :     flush : unit -> unit,
167 :     the_token_buffer : pp_token array,
168 :     the_delim_stack : delim_stack,
169 :     the_indent_stack : indent_stack,
170 :     ++ : int ref -> unit, (* increment circular buffer index *)
171 :     space_left : int ref, (* remaining columns on page *)
172 :     left_index : int ref, (* insertion index *)
173 :     right_index : int ref, (* output index *)
174 :     left_sum : int ref, (* size of strings and spaces inserted *)
175 :     right_sum : int ref, (* size of strings and spaces printed *)
176 :     panic_column : int, (* When is space_left too small *)
177 :     reset_column : int (* New start col. when space_left too small *)}
178 :    
179 :    
180 :     type ppconsumer = {consumer : string -> unit,
181 :     linewidth : int,
182 :     flush : unit -> unit}
183 :    
184 :     fun mk_ppstream {consumer,linewidth,flush} =
185 :     if (linewidth<5)
186 :     then error "linewidth too small"
187 :     else let val buf_size = 3*linewidth
188 :     in PPS{consumer = consumer,
189 :     linewidth = linewidth,
190 :     flush = flush,
191 :     the_token_buffer = array(buf_size, initial_token_value),
192 :     the_delim_stack = new_delim_stack buf_size,
193 :     the_indent_stack = mk_indent_stack (),
194 :     ++ = fn i => i := ((!i + 1) mod buf_size),
195 :     space_left = ref linewidth,
196 :     left_index = ref 0, right_index = ref 0,
197 :     left_sum = ref 0, right_sum = ref 0,
198 :     panic_column = (linewidth * 2) div 3,
199 :     reset_column = linewidth div 3}
200 :     end
201 :    
202 :     fun dest_ppstream(PPS{consumer,linewidth,flush, ...}) =
203 :     {consumer=consumer,linewidth=linewidth,flush=flush}
204 :    
205 :     local val space = #" "
206 :     fun mk_space (0,s) = String.implode s
207 :     | mk_space (n,s) = mk_space((n-1), (space::s))
208 :     val space_table = Vector.tabulate(100, fn i => mk_space(i,[]))
209 :     fun nspaces n = Vector.sub(space_table,n) handle Subscript
210 :     => if n < 0 then ""
211 :     else let val n2 = n div 2
212 :     val n2_spaces = nspaces n2
213 :     val extra = if (n = (2*n2)) then "" else " "
214 :     in String.concat [n2_spaces, n2_spaces, extra] end
215 :     in
216 :     fun cr_indent (ofn, i) = ofn ("\n"^nspaces i)
217 :     fun indent (ofn,i) = ofn (nspaces i)
218 :     end
219 :    
220 :    
221 :     (*---------------------------------------------------------------------------
222 :     Print the first member of a contiguous sequence of Begins. If there
223 :     are "processed" Begins, then take the first off the list. If there are
224 :     no processed Begins, take the last member off the "unprocessed" list.
225 :     This works because the unprocessed list is treated as a stack, the
226 :     processed list as a FIFO queue. How can an item on the unprocessed list
227 :     be printable? Because of what goes on in add_string. See there for details.
228 :     ----------------------------------------------------------------------------*)
229 :     fun print_BB (_,{Pblocks = ref [], Ublocks = ref []}) = error"print_BB"
230 :     | print_BB (PPS{the_indent_stack,linewidth,space_left=ref sp_left,...},
231 :     {Pblocks as ref({How_to_indent=CONSISTENT,Block_size,
232 :     Block_offset}::rst),
233 :     Ublocks=ref[]}) =
234 :     (push ((if (!Block_size > sp_left)
235 :     then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
236 :     else FITS),
237 :     the_indent_stack);
238 :     Pblocks := rst)
239 :     | print_BB(PPS{the_indent_stack,linewidth,space_left=ref sp_left,...},
240 :     {Pblocks as ref({Block_size,Block_offset,...}::rst),Ublocks=ref[]}) =
241 :     (push ((if (!Block_size > sp_left)
242 :     then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
243 :     else FITS),
244 :     the_indent_stack);
245 :     Pblocks := rst)
246 :     | print_BB (PPS{the_indent_stack, linewidth, space_left=ref sp_left,...},
247 :     {Ublocks,...}) = let
248 :     fun pr_end_Ublock[{How_to_indent=CONSISTENT,Block_size,Block_offset}] l =
249 :     (push ((if (!Block_size > sp_left)
250 :     then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
251 :     else FITS), the_indent_stack);
252 :     rev l)
253 :     | pr_end_Ublock [{Block_size,Block_offset,...}] l =
254 :     (push ((if (!Block_size > sp_left)
255 :     then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
256 :     else FITS), the_indent_stack);
257 :     rev l)
258 :     | pr_end_Ublock (a::rst) l = pr_end_Ublock rst (a::l)
259 :     in Ublocks := pr_end_Ublock(!Ublocks) []
260 :     end
261 :    
262 :    
263 :     (*---------------------------------------------------------------------------
264 :     Uend should always be 0 when print_E is called.
265 :     ---------------------------------------------------------------------------*)
266 :     fun print_E (_,{Pend = ref 0, Uend = ref 0}) = error "print_E"
267 :     | print_E (istack,{Pend, ...}) =
268 :     let fun pop_n_times 0 = ()
269 :     | pop_n_times n = (pop istack; pop_n_times(n-1))
270 :     in pop_n_times(!Pend); Pend := 0
271 :     end
272 :    
273 :    
274 :     (*---------------------------------------------------------------------------
275 :     "cursor" is how many spaces across the page we are.
276 :     ----------------------------------------------------------------------------*)
277 :    
278 :     fun print_token(PPS{consumer,space_left,...}, S{String,Length}) =
279 :     (consumer String; space_left := (!space_left) - Length)
280 :     | print_token(ppstrm,BB b) = print_BB(ppstrm,b)
281 :     | print_token(PPS{the_indent_stack,...},E e) =
282 :     print_E (the_indent_stack,e)
283 :     | print_token (PPS{the_indent_stack,space_left,consumer,
284 :     linewidth,panic_column, reset_column, ...},
285 :     BR{Distance_to_next_break,Number_of_blanks,Break_offset}) =
286 :     (case (top the_indent_stack)
287 :     of FITS =>
288 :     (space_left := (!space_left) - Number_of_blanks;
289 :     indent (consumer,Number_of_blanks))
290 :     | (ONE_PER_LINE cursor) =>
291 :     let val cbo = cursor + Break_offset
292 :     val new_cursor = if cbo > panic_column then reset_column
293 :     else cbo
294 :     in space_left := linewidth - new_cursor;
295 :     cr_indent (consumer,new_cursor)
296 :     end
297 :     | (PACK_ONTO_LINE cursor) =>
298 :     if (!Distance_to_next_break > (!space_left))
299 :     then let val cbo = cursor + Break_offset
300 :     val new_cursor = if cbo > panic_column then reset_column
301 :     else cbo
302 :     in space_left := linewidth - new_cursor;
303 :     cr_indent(consumer,new_cursor)
304 :     end
305 :     else (space_left := !space_left - Number_of_blanks;
306 :     indent (consumer,Number_of_blanks)))
307 :    
308 :    
309 :     fun clear_ppstream(PPS{the_token_buffer, the_delim_stack,
310 :     the_indent_stack,left_sum, right_sum,
311 :     left_index, right_index,space_left,linewidth,...}) =
312 :     let val buf_size = 3*linewidth
313 :     fun set i = if (i = buf_size) then ()
314 :     else(update(the_token_buffer,i,initial_token_value); set(i+1))
315 :     in set 0;
316 :     clear_indent_stack the_indent_stack;
317 :     reset_delim_stack the_delim_stack;
318 :     left_sum := 0; right_sum := 0;
319 :     left_index := 0; right_index := 0;
320 :     space_left := linewidth
321 :     end;
322 :    
323 :    
324 :     (*---------------------------------------------------------------------------
325 :     Move insertion head to right unless adding a BB and already at a BB,
326 :     or unless adding an E and already at an E.
327 :     ---------------------------------------------------------------------------*)
328 :     fun BB_inc_right_index(PPS{the_token_buffer, right_index, ++,...})=
329 :     case (the_token_buffer sub (!right_index))
330 :     of (BB _) => ()
331 :     | _ => ++right_index
332 :    
333 :     fun E_inc_right_index(PPS{the_token_buffer,right_index, ++,...})=
334 :     case (the_token_buffer sub (!right_index))
335 :     of (E _) => ()
336 :     | _ => ++right_index
337 :    
338 :    
339 :     fun pointers_coincide(PPS{left_index,right_index,the_token_buffer,...}) =
340 :     (!left_index = !right_index) andalso
341 :     (case (the_token_buffer sub (!left_index))
342 :     of (BB {Pblocks = ref [], Ublocks = ref []}) => true
343 :     | (BB _) => false
344 :     | (E {Pend = ref 0, Uend = ref 0}) => true
345 :     | (E _) => false
346 :     | _ => true)
347 :    
348 :     fun advance_left (ppstrm as PPS{consumer,left_index,left_sum,
349 :     the_token_buffer,++,...},
350 :     instr) =
351 :     let val NEG = ~1
352 :     val POS = 0
353 :     fun inc_left_sum (BR{Number_of_blanks, ...}) =
354 :     left_sum := (!left_sum) + Number_of_blanks
355 :     | inc_left_sum (S{Length, ...}) = left_sum := (!left_sum) + Length
356 :     | inc_left_sum _ = ()
357 :    
358 :     fun last_size [{Block_size, ...}:block_info] = !Block_size
359 :     | last_size (_::rst) = last_size rst
360 :     fun token_size (S{Length, ...}) = Length
361 :     | token_size (BB b) =
362 :     (case b
363 :     of {Pblocks = ref[], Ublocks = ref[]} => error "BB_size"
364 :     | {Pblocks as ref(_::_),Ublocks=ref[]} => POS
365 :     | {Ublocks, ...} => last_size (!Ublocks))
366 :     | token_size (E{Pend=ref 0, Uend=ref 0}) = error"token_size.E"
367 :     | token_size (E{Pend = ref 0, ...}) = NEG
368 :     | token_size (E _) = POS
369 :     | token_size (BR {Distance_to_next_break, ...}) = !Distance_to_next_break
370 :     fun loop (instr) =
371 :     if (token_size instr < 0) (* synchronization point; cannot advance *)
372 :     then ()
373 :     else (print_token(ppstrm,instr);
374 :     inc_left_sum instr;
375 :     if (pointers_coincide ppstrm) then ()
376 :     else (* increment left index *)
377 :    
378 :     (*-----------------------------------------------------------------------
379 :     When this arm is entered, we know that the left_index has not yet
380 :     caught up to the right_index. If we are at a BB or an E, we can
381 :     increment left_index if there is no work to be done, i.e., all Begins
382 :     or Ends have been dealt with. Also, we should do some housekeeping and
383 :     clear the buffer at left_index, otherwise we can get errors when
384 :     left_index catches up to right_index and we reset the indices to 0.
385 :     (We might find ourselves adding a BB to an "old" BB, with the result
386 :     that the index is not pushed onto the delim_stack. This can lead to
387 :     mangled output.)
388 :     -----------------------------------------------------------------------*)
389 :     (case (the_token_buffer sub (!left_index))
390 :     of (BB {Pblocks = ref [], Ublocks = ref []}) =>
391 :     (update(the_token_buffer, !left_index,initial_token_value);
392 :     ++left_index)
393 :     | (BB _) => ()
394 :     | (E {Pend = ref 0, Uend = ref 0}) =>
395 :     (update(the_token_buffer,!left_index, initial_token_value);
396 :     ++left_index)
397 :     | (E _) => ()
398 :     | _ => ++left_index;loop (the_token_buffer sub (!left_index))))
399 :     in loop instr
400 :     end
401 :    
402 :    
403 :     fun begin_block (ppstrm as PPS{the_token_buffer, the_delim_stack,left_index,
404 :     left_sum, right_index, right_sum,...})
405 :     style offset =
406 :     (if (delim_stack_is_empty the_delim_stack)
407 :     then (left_index := 0;
408 :     left_sum := 1;
409 :     right_index := 0;
410 :     right_sum := 1)
411 :     else BB_inc_right_index ppstrm;
412 :     case (the_token_buffer sub (!right_index))
413 :     of (BB {Ublocks, ...}) =>
414 :     Ublocks := {Block_size = ref (~(!right_sum)),
415 :     Block_offset = offset,
416 :     How_to_indent = style}::(!Ublocks)
417 :     | _ => (update(the_token_buffer, !right_index,
418 :     BB{Pblocks = ref [],
419 :     Ublocks = ref [{Block_size = ref (~(!right_sum)),
420 :     Block_offset = offset,
421 :     How_to_indent = style}]});
422 :     push_delim_stack (!right_index, the_delim_stack)))
423 :    
424 :    
425 :     fun end_block(ppstrm as PPS{the_token_buffer,the_delim_stack,right_index,...})=
426 :     if (delim_stack_is_empty the_delim_stack)
427 :     then print_token(ppstrm,(E{Pend = ref 1, Uend = ref 0}))
428 :     else (E_inc_right_index ppstrm;
429 :     case (the_token_buffer sub (!right_index))
430 :     of (E{Uend, ...}) => inc Uend
431 :     | _ => (update(the_token_buffer,!right_index,
432 :     E{Uend = ref 1, Pend = ref 0});
433 :     push_delim_stack (!right_index, the_delim_stack)))
434 :    
435 :     local
436 :     fun check_delim_stack(PPS{the_token_buffer,the_delim_stack,right_sum,...}) =
437 :     let fun check k =
438 :     if (delim_stack_is_empty the_delim_stack) then ()
439 :     else case(the_token_buffer sub (top_delim_stack the_delim_stack))
440 :     of BB{Ublocks as ref ((b as {Block_size, ...})::rst), Pblocks}
441 :     => if (k>0)
442 :     then (Block_size := !right_sum + !Block_size;
443 :     Pblocks := b :: (!Pblocks);
444 :     Ublocks := rst;
445 :     if (List.length rst = 0)
446 :     then pop_delim_stack the_delim_stack else ();
447 :     check(k-1))
448 :     else ()
449 :     | E{Pend,Uend}
450 :     => (Pend := (!Pend) + (!Uend);
451 :     Uend := 0;
452 :     pop_delim_stack the_delim_stack;
453 :     check(k + !Pend))
454 :     | BR{Distance_to_next_break, ...}
455 :     => (Distance_to_next_break := !right_sum +
456 :     !Distance_to_next_break;
457 :     pop_delim_stack the_delim_stack;
458 :     if (k>0) then check k else ())
459 :     | _ => error "check_delim_stack.catchall"
460 :     in check 0
461 :     end
462 :     in
463 :    
464 :     fun add_break (ppstrm as PPS{the_token_buffer,the_delim_stack,left_index,
465 :     right_index,left_sum,right_sum, ++, ...})
466 :     (n,break_offset) =
467 :     (if (delim_stack_is_empty the_delim_stack)
468 :     then (left_index := 0; right_index := 0;
469 :     left_sum := 1; right_sum := 1)
470 :     else ++right_index;
471 :     update(the_token_buffer, !right_index,
472 :     BR{Distance_to_next_break = ref (~(!right_sum)),
473 :     Number_of_blanks = n,
474 :     Break_offset = break_offset});
475 :     check_delim_stack ppstrm;
476 :     right_sum := (!right_sum) + n;
477 :     push_delim_stack (!right_index,the_delim_stack))
478 :    
479 :     fun flush_ppstream0(ppstrm as PPS{the_delim_stack,the_token_buffer, flush,
480 :     left_index,...}) =
481 :     (if (delim_stack_is_empty the_delim_stack)
482 :     then ()
483 :     else (check_delim_stack ppstrm;
484 :     advance_left(ppstrm, the_token_buffer sub (!left_index)));
485 :     flush())
486 :    
487 :     end (* local *)
488 :    
489 :    
490 :     fun flush_ppstream ppstrm =
491 :     (flush_ppstream0 ppstrm;
492 :     clear_ppstream ppstrm)
493 :    
494 :     fun add_string (ppstrm as PPS{the_token_buffer,the_delim_stack,consumer,
495 :     right_index,right_sum,left_sum,
496 :     left_index,space_left,++,...})
497 :     s =
498 :     let fun fnl [{Block_size, ...}:block_info] = Block_size := INFINITY
499 :     | fnl (_::rst) = fnl rst
500 :    
501 :     fun set(dstack,BB{Ublocks as ref[{Block_size,...}:block_info],...}) =
502 :     (pop_bottom_delim_stack dstack;
503 :     Block_size := INFINITY)
504 :     | set (_,BB {Ublocks = ref(_::rst), ...}) = fnl rst
505 :     | set (dstack, E{Pend,Uend}) =
506 :     (Pend := (!Pend) + (!Uend);
507 :     Uend := 0;
508 :     pop_bottom_delim_stack dstack)
509 :     | set (dstack,BR{Distance_to_next_break,...}) =
510 :     (pop_bottom_delim_stack dstack;
511 :     Distance_to_next_break := INFINITY)
512 :     | set _ = raise (PP_FAIL "add_string.set")
513 :    
514 :     fun check_stream () =
515 :     if ((!right_sum - !left_sum) > !space_left)
516 :     then if (delim_stack_is_empty the_delim_stack)
517 :     then ()
518 :     else let val i = bottom_delim_stack the_delim_stack
519 :     in if (!left_index = i)
520 :     then set (the_delim_stack, the_token_buffer sub i)
521 :     else ();
522 :     advance_left(ppstrm,
523 :     the_token_buffer sub (!left_index));
524 :     if (pointers_coincide ppstrm)
525 :     then ()
526 :     else check_stream ()
527 :     end
528 :     else ()
529 :    
530 :     val slen = String.size s
531 :     val S_token = S{String = s, Length = slen}
532 :    
533 :     in if (delim_stack_is_empty the_delim_stack)
534 :     then print_token(ppstrm,S_token)
535 :     else (++right_index;
536 :     update(the_token_buffer, !right_index, S_token);
537 :     right_sum := (!right_sum)+slen;
538 :     check_stream ())
539 :     end
540 :    
541 :    
542 :     (* Derived form. The +2 is for peace of mind *)
543 :     fun add_newline (ppstrm as PPS{linewidth, ...}) =
544 :     add_break ppstrm (linewidth+2,0)
545 :    
546 :     (*---------------------------------------------------------------------------
547 :     * Builds a ppstream, sends pretty printing commands called in f to
548 :     * the ppstream, then flushes ppstream.
549 :     *---------------------------------------------------------------------------*)
550 :     fun with_pp ppconsumer ppfn =
551 :     let val ppstrm = mk_ppstream ppconsumer
552 :     in ppfn ppstrm;
553 :     flush_ppstream0 ppstrm
554 :     end
555 :    
556 :     fun pp_to_string linewidth ppfn ob =
557 :     let val l = ref ([]:string list)
558 :     fun attach s = l := (s :: !l)
559 :     in with_pp {consumer = attach, linewidth=linewidth, flush = fn()=>()}
560 :     (fn ppstrm => ppfn ppstrm ob);
561 :     String.concat(List.rev(!l))
562 :     end
563 :    
564 :    
565 :     (*---------------------------------------------------------------------------
566 :     Derived forms for making ppstreams that observe system parameters.
567 :    
568 :     fun stdOut_consumer() =
569 :     let val {say,flush} = !Control.Print.out
570 :     in {consumer=say, flush=flush,
571 :     linewidth = !Control.Print.linewidth}
572 :     end;
573 :    
574 :     val stdOut_ppstream = mk_ppstream o stdOut_consumer;
575 :    
576 :     ----------------------------------------------------------------------------*)
577 :    
578 :     end (* PrettyPrint *)
579 :    

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0