1(* PP -- Oppen-style prettyprinters. 2 * 3 * Modified for Moscow ML from SML/NJ Library version 0.2 4 * 5 * COPYRIGHT (c) 1992 by AT&T Bell Laboratories. 6 * See file mosml/copyrght/copyrght.att for details. 7 *) 8 9(* the functions and data for actually doing printing. *) 10structure OldPP :> OldPP = 11struct 12 13datatype frag = datatype HOLPP.frag 14type 'a quotation = 'a frag list 15 16 17open Array 18infix 9 sub 19 20(* the queue library, formerly in unit Ppqueue *) 21 22datatype Qend = Qback | Qfront 23 24exception QUEUE_FULL 25exception QUEUE_EMPTY 26exception REQUESTED_QUEUE_SIZE_TOO_SMALL 27 28local 29 fun ++ i n = (i + 1) mod n 30 fun -- i n = (i - 1) mod n 31in 32 33abstype 'a queue = QUEUE of {elems: 'a array, (* the contents *) 34 front: int ref, 35 back: int ref, 36 size: int} (* fixed size of element array *) 37with 38 39 fun is_empty (QUEUE{front=f, back=b,...}) = (!f = ~1 andalso !b = ~1) 40 41 fun mk_queue n init_val = 42 if (n < 2) 43 then raise REQUESTED_QUEUE_SIZE_TOO_SMALL 44 else QUEUE{elems=array(n, init_val), front=ref ~1, back=ref ~1, size=n} 45 46 fun clear_queue (QUEUE{front,back,...}) = (front := ~1; back := ~1) 47 48 fun queue_at Qfront (QUEUE{elems,front,...}) = elems sub !front 49 | queue_at Qback (QUEUE{elems,back,...}) = elems sub !back 50 51 fun en_queue Qfront item (Q as QUEUE{elems,front,back,size}) = 52 if (is_empty Q) 53 then (front := 0; back := 0; 54 update(elems,0,item)) 55 else let val i = --(!front) size 56 in if (i = !back) 57 then raise QUEUE_FULL 58 else (update(elems,i,item); front := i) 59 end 60 | en_queue Qback item (Q as QUEUE{elems,front,back,size}) = 61 if (is_empty Q) 62 then (front := 0; back := 0; 63 update(elems,0,item)) 64 else let val i = ++(!back) size 65 in if (i = !front) 66 then raise QUEUE_FULL 67 else (update(elems,i,item); back := i) 68 end 69 70 fun de_queue Qfront (Q as QUEUE{front,back,size,...}) = 71 if (!front = !back) (* unitary queue *) 72 then clear_queue Q 73 else front := ++(!front) size 74 | de_queue Qback (Q as QUEUE{front,back,size,...}) = 75 if (!front = !back) 76 then clear_queue Q 77 else back := --(!back) size 78 79end (* abstype queue *) 80end (* local *) 81 82 83(* exception PP_FAIL of string *) 84datatype break_style = datatype HOLPP.break_style 85 86datatype break_info 87 = FITS 88 | PACK_ONTO_LINE of int 89 | ONE_PER_LINE of int 90 91(* Some global values *) 92val INFINITY = 999999 93 94abstype indent_stack = Istack of break_info list ref 95with 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 => raise Fail "PP-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 => raise Fail "PP-error: pop: badly formed block" 106 | _::rest => stk := rest 107end 108 109(* The delim_stack is used to compute the size of blocks. It is 110 a stack of indices into the token buffer. The indices only point to 111 BBs, Es, and BRs. We push BBs and Es onto the stack until a BR 112 is encountered. Then we compute sizes and pop. When we encounter 113 a BR in the middle of a block, we compute the Distance_to_next_break 114 of the previous BR in the block, if there was one. 115 116 We need to be able to delete from the bottom of the delim_stack, so 117 we use a queue, treated with a stack discipline, i.e., we only add 118 items at the head of the queue, but can delete from the front or 119 back of the queue. 120*) 121abstype delim_stack = Dstack of int queue 122with 123 fun new_delim_stack i = Dstack(mk_queue i ~1) 124 fun reset_delim_stack (Dstack q) = clear_queue q 125 126 fun pop_delim_stack (Dstack d) = de_queue Qfront d 127 fun pop_bottom_delim_stack (Dstack d) = de_queue Qback d 128 129 fun push_delim_stack(i,Dstack d) = en_queue Qfront i d 130 fun top_delim_stack (Dstack d) = queue_at Qfront d 131 fun bottom_delim_stack (Dstack d) = queue_at Qback d 132 fun delim_stack_is_empty (Dstack d) = is_empty d 133end 134 135 136type block_info = { Block_size : int ref, 137 Block_offset : int, 138 How_to_indent : break_style } 139 140 141(* Distance_to_next_break includes Number_of_blanks. Break_offset is 142 a local offset for the break. BB represents a sequence of contiguous 143 Begins. E represents a sequence of contiguous Ends. 144*) 145datatype pp_token 146 = S of {String : string, Length : int} 147 | BB of {Pblocks : block_info list ref, (* Processed *) 148 Ublocks : block_info list ref} (* Unprocessed *) 149 | E of {Pend : int ref, Uend : int ref} 150 | BR of {Distance_to_next_break : int ref, 151 Number_of_blanks : int, 152 Break_offset : int} 153 154 155(* The initial values in the token buffer *) 156val initial_token_value = S{String = "", Length = 0} 157 158datatype ppstream0 = 159 PPS of 160 {consumer : string -> unit, 161 linewidth : int, 162 flush : unit -> unit, 163 the_token_buffer : pp_token array, 164 the_delim_stack : delim_stack, 165 the_indent_stack : indent_stack, 166 ++ : int ref -> unit, (* increment circular buffer index *) 167 space_left : int ref, (* remaining columns on page *) 168 left_index : int ref, (* insertion index *) 169 right_index : int ref, (* output index *) 170 left_sum : int ref, (* size of strings and spaces inserted *) 171 right_sum : int ref} (* size of strings and spaces printed *) 172 173fun lineWidth0 (PPS {linewidth, ...}) = linewidth 174 175type ppconsumer = {consumer : string -> unit, 176 linewidth : int, 177 flush : unit -> unit} 178 179fun safe_consumer ofn = let 180 val output_stack = ref ([]:string list) 181 fun doit s = let 182 in 183 if String.size s = 0 then () 184 else if String.sub(s,0) = #"\n" then 185 (output_stack := []; ofn ("\n"); doit(String.extract(s,1,NONE))) 186 else if CharVector.all Char.isSpace s then 187 output_stack := s :: !output_stack 188 else (List.app ofn (List.rev (!output_stack)); 189 output_stack := []; 190 ofn(s)) 191 end 192in 193 doit 194end 195 196 197 198 199local 200 val space = " " 201 fun mk_space (0,s) = String.concat s 202 | mk_space (n,s) = mk_space((n-1), (space::s)) 203 val space_table = Vector.tabulate(100, fn i => mk_space(i,[])) 204 fun nspaces n = Vector.sub(space_table, n) 205 handle General.Subscript => 206 if n < 0 207 then "" 208 else let val n2 = n div 2 209 val n2_spaces = nspaces n2 210 val extra = if (n = (2*n2)) then "" else space 211 in String.concat [n2_spaces, n2_spaces, extra] 212 end 213in 214 fun cr_indent (ofn, i) = ofn ("\n"^(nspaces i)) 215 fun indent (ofn,i) = ofn (nspaces i) 216end 217 218 219(* Print a the first member of a contiguous sequence of Begins. If there 220 are "processed" Begins, then take the first off the list. If there are 221 no processed Begins, take the last member off the "unprocessed" list. 222 This works because the unprocessed list is treated as a stack, the 223 processed list as a FIFO queue. How can an item on the unprocessed list 224 be printable? Because of what goes on in add_string. See there for details. 225*) 226 227fun print_BB (PPS {the_indent_stack,linewidth,space_left,...}, {Pblocks, Ublocks}) = 228 let val sp_left = !space_left in 229 case (!Pblocks, !Ublocks) of 230 ([], []) => 231 raise Fail "PP-error: print_BB" 232 | ({How_to_indent=CONSISTENT,Block_size, Block_offset}::rst, []) => 233 (push ((if (!Block_size > sp_left) 234 then ONE_PER_LINE (linewidth - (sp_left - Block_offset)) 235 else FITS), 236 the_indent_stack); 237 Pblocks := rst) 238 | ({Block_size,Block_offset,...}::rst, []) => 239 (push ((if (!Block_size > sp_left) 240 then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset)) 241 else FITS), 242 the_indent_stack); 243 Pblocks := rst) 244 | (_, Ubl) => 245 let fun pr_end_Ublock [{How_to_indent=CONSISTENT,Block_size,Block_offset}] l = 246 (push ((if (!Block_size > sp_left) 247 then ONE_PER_LINE (linewidth - (sp_left - Block_offset)) 248 else FITS), 249 the_indent_stack); 250 List.rev l) 251 | pr_end_Ublock [{Block_size,Block_offset,...}] l = 252 (push ((if (!Block_size > sp_left) 253 then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset)) 254 else FITS), 255 the_indent_stack); 256 List.rev l) 257 | pr_end_Ublock (a::rst) l = pr_end_Ublock rst (a::l) 258 | pr_end_Ublock _ _ = 259 raise Fail "PP-error: print_BB: internal error" 260 in Ublocks := pr_end_Ublock Ubl [] 261 end 262end 263 264(* Uend should always be 0 when print_E is called. *) 265fun print_E (istack,{Pend, Uend}) = 266 if !Pend = 0 andalso !Uend = 0 267 then raise Fail "PP-error: print_E" 268 else 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(* "cursor" is how many spaces across the page we are. *) 275 276fun print_token(PPS{consumer,space_left,...}, S{String,Length}) = 277 (consumer String; 278 space_left := (!space_left) - Length) 279 | print_token(ppstrm,BB b) = print_BB(ppstrm,b) 280 | print_token(PPS{the_indent_stack,...},E e) = 281 print_E (the_indent_stack,e) 282 | print_token (PPS{the_indent_stack,space_left,consumer,linewidth,...}, 283 BR{Distance_to_next_break,Number_of_blanks,Break_offset}) = 284 (case (top the_indent_stack) 285 of FITS => 286 (space_left := (!space_left) - Number_of_blanks; 287 indent (consumer,Number_of_blanks)) 288 | (ONE_PER_LINE cursor) => 289 let val new_cursor = cursor + Break_offset 290 in space_left := linewidth - new_cursor; 291 cr_indent (consumer,new_cursor) 292 end 293 | (PACK_ONTO_LINE cursor) => 294 if (!Distance_to_next_break > (!space_left)) 295 then let val new_cursor = cursor + Break_offset 296 in space_left := linewidth - new_cursor; 297 cr_indent(consumer,new_cursor) 298 end 299 else (space_left := !space_left - Number_of_blanks; 300 indent (consumer,Number_of_blanks))) 301 302 303fun clear_ppstream0(pps : ppstream0) = 304 let val PPS{the_token_buffer, the_delim_stack, 305 the_indent_stack,left_sum, right_sum, 306 left_index, right_index,space_left,linewidth,...} 307 = pps 308 val buf_size = 3*linewidth 309 fun set i = 310 if (i = buf_size) 311 then () 312 else (update(the_token_buffer,i,initial_token_value); 313 set (i+1)) 314 in set 0; 315 clear_indent_stack the_indent_stack; 316 reset_delim_stack the_delim_stack; 317 left_sum := 0; right_sum := 0; 318 left_index := 0; right_index := 0; 319 space_left := linewidth 320 end 321 322 323(* Move insertion head to right unless adding a BB and already at a BB, 324 or unless adding an E and already at an E. 325*) 326fun BB_inc_right_index(PPS{the_token_buffer, right_index, ++,...})= 327 case (the_token_buffer sub (!right_index)) 328 of (BB _) => () 329 | _ => ++right_index 330 331fun E_inc_right_index(PPS{the_token_buffer,right_index, ++,...})= 332 case (the_token_buffer sub (!right_index)) 333 of (E _) => () 334 | _ => ++right_index 335 336 337fun pointers_coincide(PPS{left_index,right_index,the_token_buffer,...}) = 338 (!left_index = !right_index) andalso 339 (case (the_token_buffer sub (!left_index)) 340 of (BB {Pblocks = Pb, Ublocks = Ub}) => (case (!Pb, !Ub) of ([], []) => true | _ => false) 341 | (E {Pend = Pe, Uend = Ue}) => !Pe = 0 andalso !Ue = 0 342 | _ => true) 343 344fun advance_left (ppstrm as PPS{consumer,left_index,left_sum, 345 the_token_buffer,++,...}, 346 instr) = 347 let val NEG = ~1 348 val POS = 0 349 fun inc_left_sum (BR{Number_of_blanks, ...}) = 350 left_sum := (!left_sum) + Number_of_blanks 351 | inc_left_sum (S{Length, ...}) = left_sum := (!left_sum) + Length 352 | inc_left_sum _ = () 353 354 fun last_size [{Block_size, ...}:block_info] = !Block_size 355 | last_size (_::rst) = last_size rst 356 | last_size _ = raise Fail "PP-error: last_size: internal error" 357 fun token_size (S{Length, ...}) = Length 358 | token_size (BB {Pblocks, Ublocks}) = 359 (case (!Pblocks, !Ublocks) of 360 ([], []) => raise Fail "PP-error: BB_size" 361 | (_::_, []) => POS 362 | (_, ub) => last_size ub) 363 | token_size (E{Pend, Uend}) = 364 (case (!Pend, !Uend) of 365 (0, 0) => 366 raise Fail "PP-error: token_size.E" 367 | (0, _) => NEG 368 | _ => 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) 376 then () 377 else (* increment left index *) 378 379 (* When this is evaluated, 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, Ublocks}) => 391 (case (!Pblocks, !Ublocks) of ([], []) => 392 (update(the_token_buffer,!left_index, 393 initial_token_value); 394 ++left_index) 395 | _ => ()) 396 | (E {Pend, Uend}) => 397 if !Pend = 0 andalso !Uend = 0 then 398 (update(the_token_buffer,!left_index, 399 initial_token_value); 400 ++left_index) 401 else () 402 | _ => ++left_index; 403 loop (the_token_buffer sub (!left_index)))) 404 in loop instr 405 end 406 407 408fun begin_block0 (ppstrm : ppstream0) style offset = 409 let val PPS{the_token_buffer, the_delim_stack,left_index, 410 left_sum, right_index, right_sum,...} 411 = ppstrm 412 in 413 (if (delim_stack_is_empty the_delim_stack) 414 then (left_index := 0; 415 left_sum := 1; 416 right_index := 0; 417 right_sum := 1) 418 else BB_inc_right_index ppstrm; 419 case (the_token_buffer sub (!right_index)) 420 of (BB {Ublocks, ...}) => 421 Ublocks := {Block_size = ref (~(!right_sum)), 422 Block_offset = offset, 423 How_to_indent = style}::(!Ublocks) 424 | _ => (update(the_token_buffer, !right_index, 425 BB{Pblocks = ref [], 426 Ublocks = ref [{Block_size = ref (~(!right_sum)), 427 Block_offset = offset, 428 How_to_indent = style}]}); 429 push_delim_stack (!right_index, the_delim_stack))) 430 end 431 432fun end_block0(ppstrm : ppstream0) = 433 let val PPS{the_token_buffer,the_delim_stack,right_index,...} 434 = ppstrm 435 in 436 if (delim_stack_is_empty the_delim_stack) 437 then print_token(ppstrm,(E{Pend = ref 1, Uend = ref 0})) 438 else (E_inc_right_index ppstrm; 439 case (the_token_buffer sub (!right_index)) 440 of (E{Uend, ...}) => Uend := !Uend + 1 441 | _ => (update(the_token_buffer,!right_index, 442 E{Uend = ref 1, Pend = ref 0}); 443 push_delim_stack (!right_index, the_delim_stack))) 444 end 445 446local 447 fun check_delim_stack(PPS{the_token_buffer,the_delim_stack,right_sum,...}) = 448 let fun check k = 449 if (delim_stack_is_empty the_delim_stack) 450 then () 451 else case(the_token_buffer sub (top_delim_stack the_delim_stack)) 452 of (BB{Ublocks, Pblocks}) => 453 (case !Pblocks of 454 ((b as {Block_size, ...})::rst) => 455 if (k>0) 456 then (Block_size := !right_sum + !Block_size; 457 Pblocks := b :: (!Pblocks); 458 Ublocks := rst; 459 if (List.length rst = 0) 460 then pop_delim_stack the_delim_stack 461 else (); 462 check(k-1)) 463 else () 464 | _ => raise Fail "PP-error: check_delim_stack.catch empty !Pblocks") 465 | (E{Pend,Uend}) => 466 (Pend := (!Pend) + (!Uend); 467 Uend := 0; 468 pop_delim_stack the_delim_stack; 469 check(k + !Pend)) 470 | (BR{Distance_to_next_break, ...}) => 471 (Distance_to_next_break := 472 !right_sum + !Distance_to_next_break; 473 pop_delim_stack the_delim_stack; 474 if (k>0) 475 then check k 476 else ()) 477 | _ => raise Fail "PP-error: check_delim_stack.catchall" 478 in check 0 479 end 480in 481 482 fun add_break0 (ppstrm : ppstream0) (n, break_offset) = 483 let val PPS{the_token_buffer,the_delim_stack,left_index, 484 right_index,left_sum,right_sum, ++, ...} 485 = ppstrm 486 in 487 (if (delim_stack_is_empty the_delim_stack) 488 then (left_index := 0; right_index := 0; 489 left_sum := 1; right_sum := 1) 490 else ++right_index; 491 update(the_token_buffer, !right_index, 492 BR{Distance_to_next_break = ref (~(!right_sum)), 493 Number_of_blanks = n, 494 Break_offset = break_offset}); 495 check_delim_stack ppstrm; 496 right_sum := (!right_sum) + n; 497 push_delim_stack (!right_index,the_delim_stack)) 498 end 499 500 fun flush_ppstream0(ppstrm : ppstream0) = 501 let val PPS{the_delim_stack,the_token_buffer, flush, left_index,...} 502 = ppstrm 503 in 504 (if (delim_stack_is_empty the_delim_stack) 505 then () 506 else (check_delim_stack ppstrm; 507 advance_left(ppstrm, the_token_buffer sub (!left_index))); 508 flush()) 509 end 510 511end (* local *) 512 513 514fun flush_ppstream' ppstrm = 515 (flush_ppstream0 ppstrm; 516 clear_ppstream0 ppstrm) 517 518fun add_stringsz0 (pps : ppstream0) (s,slen) = 519 let val PPS{the_token_buffer,the_delim_stack,consumer, 520 right_index,right_sum,left_sum, 521 left_index,space_left,++,...} 522 = pps 523 fun fnl [{Block_size, ...}:block_info] = Block_size := INFINITY 524 | fnl (_::rst) = fnl rst 525 | fnl _ = raise Fail "PP-error: fnl: internal error" 526 527 fun set(dstack,BB{Ublocks, ...}) = 528 (case !Ublocks of 529 [{Block_size,...}:block_info] => 530 (pop_bottom_delim_stack dstack; 531 Block_size := INFINITY) 532 | (_::rst) => fnl rst 533 | _ => raise (Fail "PP-error: add_string.set")) 534 | set (dstack, E{Pend,Uend}) = 535 (Pend := (!Pend) + (!Uend); 536 Uend := 0; 537 pop_bottom_delim_stack dstack) 538 | set (dstack,BR{Distance_to_next_break,...}) = 539 (pop_bottom_delim_stack dstack; 540 Distance_to_next_break := INFINITY) 541 | set _ = raise (Fail "PP-error: add_string.set") 542 543 fun check_stream () = 544 if ((!right_sum - !left_sum) > !space_left) 545 then if (delim_stack_is_empty the_delim_stack) 546 then () 547 else let val i = bottom_delim_stack the_delim_stack 548 in if (!left_index = i) 549 then set (the_delim_stack, the_token_buffer sub i) 550 else (); 551 advance_left(pps, the_token_buffer sub (!left_index)); 552 if (pointers_coincide pps) then () 553 else check_stream () 554 end 555 else () 556 557 val S_token = S{String = s, Length = slen} 558 559 in if (delim_stack_is_empty the_delim_stack) 560 then print_token(pps,S_token) 561 else (++right_index; 562 update(the_token_buffer, !right_index, S_token); 563 right_sum := (!right_sum)+slen; 564 check_stream ()) 565 end 566 567 568type ppstream_interface = 569{ add_stringsz : (string * int) -> unit, 570 add_break : int * int -> unit, 571 begin_block : break_style -> int -> unit, 572 clear_ppstream : unit -> unit, 573 end_block : unit -> unit, 574 flush : unit -> unit, 575 linewidth : int} 576 577 578datatype ppstream = OLD of ppstream0 579 | NEW of ppstream_interface 580 581val pps_from_iface = NEW 582 583fun add_break (OLD pps) nm = add_break0 pps nm 584 | add_break (NEW {add_break = bk,...}) nm = bk nm 585 586fun begin_block (OLD pps) bs i = begin_block0 pps bs i 587 | begin_block (NEW{begin_block = bb, ...}) bs i = bb bs i 588 589fun end_block (OLD pps) = end_block0 pps 590 | end_block (NEW {end_block = eb, ...}) = eb() 591 592fun clear_ppstream (OLD pps) = clear_ppstream0 pps 593 | clear_ppstream (NEW {clear_ppstream = cp,...}) = cp() 594 595fun flush_ppstream (OLD pps) = flush_ppstream' pps 596 | flush_ppstream (NEW {flush,...}) = flush() 597 598fun mk_ppstream {consumer,linewidth,flush} = 599 if (linewidth<5) then raise Fail "PP-error: linewidth too_small" 600 else let 601 val buf_size = 3*linewidth 602 in 603 OLD (PPS{consumer = safe_consumer consumer, 604 linewidth = linewidth, 605 flush = flush, 606 the_token_buffer = array(buf_size, initial_token_value), 607 the_delim_stack = new_delim_stack buf_size, 608 the_indent_stack = mk_indent_stack (), 609 ++ = fn i => i := ((!i + 1) mod buf_size), 610 space_left = ref linewidth, 611 left_index = ref 0, right_index = ref 0, 612 left_sum = ref 0, right_sum = ref 0}) 613 end 614 615 616(* Derived form. Builds a ppstream, sends pretty printing commands called in 617 f to the ppstream, then flushes ppstream. 618*) 619val catch_withpp_err = ref true 620 621fun with_pp ppconsumer ppfn = let 622 val ppstrm = mk_ppstream ppconsumer 623in 624 ppfn ppstrm; 625 flush_ppstream ppstrm 626end handle e as Fail msg => 627 if !catch_withpp_err then 628 TextIO.print (">>>> Pretty-printer failure: " ^ msg ^ "\n") 629 else raise e 630 631 632 633fun pp_to_string linewidth ppfn ob = 634 let val l = ref ([]:string list) 635 fun attach s = l := (s::(!l)) 636 in with_pp {consumer = attach, linewidth=linewidth, flush = fn()=>()} 637 (fn ppstrm => ppfn ppstrm ob); 638 String.concat(List.rev(!l)) 639 end 640 641fun lineWidth (OLD pps) = lineWidth0 pps 642 | lineWidth (NEW {linewidth, ...}) = linewidth 643 644fun add_stringsz (OLD pps) ssz = add_stringsz0 pps ssz 645 | add_stringsz (NEW {add_stringsz = add,...}) ssz = add ssz 646 647fun add_string pps s = let 648 val slen = UTF8.size s 649in 650 add_stringsz pps (s,slen) 651end 652 653(* Derived form. The +2 is for peace of mind *) 654fun add_newline (pps : ppstream) = 655 let val lw = lineWidth pps in add_break pps (lw+2,0) end 656 657fun pr_list pfun dfun bfun = 658 let 659 fun pr [] = () 660 | pr [i] = pfun i 661 | pr (i :: rst) = (pfun i; dfun (); bfun (); pr rst) 662 in 663 pr 664 end 665 666fun with_ppstream ppstrm = 667 {add_string = add_string ppstrm, 668 add_break = add_break ppstrm, 669 begin_block = begin_block ppstrm, 670 end_block = fn () => end_block ppstrm, 671 add_newline = fn () => add_newline ppstrm, 672 clear_ppstream = fn () => clear_ppstream ppstrm, 673 flush_ppstream = fn () => flush_ppstream ppstrm} 674 675end; (* struct *) 676