1signature OldPP = 2sig 3(* PP -- pretty-printing -- from the SML/NJ library *) 4 5type ppstream 6type ppconsumer = { consumer : string -> unit, 7 linewidth : int, 8 flush : unit -> unit } 9 10datatype break_style = datatype HOLPP.break_style 11 12type ppstream_interface = 13 { add_stringsz : (string * int) -> unit, 14 add_break : int * int -> unit, 15 begin_block : break_style -> int -> unit, 16 clear_ppstream : unit -> unit, 17 end_block : unit -> unit, 18 flush : unit -> unit, 19 linewidth : int} 20 21datatype frag = datatype HOLPP.frag 22type 'a quotation = 'a frag list 23 24val mk_ppstream : ppconsumer -> ppstream 25val pps_from_iface : ppstream_interface -> ppstream 26val add_break : ppstream -> int * int -> unit 27val add_newline : ppstream -> unit 28val add_string : ppstream -> string -> unit 29val add_stringsz : ppstream -> (string * int) -> unit 30val begin_block : ppstream -> break_style -> int -> unit 31val end_block : ppstream -> unit 32val clear_ppstream : ppstream -> unit 33val flush_ppstream : ppstream -> unit 34val with_pp : ppconsumer -> (ppstream -> unit) -> unit 35val pp_to_string : int -> (ppstream -> 'a -> unit) -> 'a -> string 36val lineWidth : ppstream -> int 37val catch_withpp_err : bool ref 38 39val pr_list : ('a -> unit) -> (unit -> 'b) -> (unit -> 'c) -> 'a list -> 40 unit 41 42val with_ppstream : ppstream -> 43 {add_break : int * int -> unit, 44 add_newline : unit -> unit, 45 add_string : string -> unit, 46 begin_block : HOLPP.break_style -> int -> unit, 47 clear_ppstream : unit -> unit, 48 end_block : unit -> unit, 49 flush_ppstream : unit -> unit} 50 51(* 52 This structure provides tools for creating customized Oppen-style 53 pretty-printers, based on the type ppstream. A ppstream is an 54 output stream that contains prettyprinting commands. The commands 55 are placed in the stream by various function calls listed below. 56 57 There following primitives add commands to the stream: 58 begin_block, end_block, add_string, add_break, and add_newline. 59 All calls to add_string, add_break, and add_newline must happen 60 between a pair of calls to begin_block and end_block must be 61 properly nested dynamically. All calls to begin_block and 62 end_block must be properly nested (dynamically). 63 64 [ppconsumer] is the type of sinks for pretty-printing. A value of 65 type ppconsumer is a record 66 { consumer : string -> unit, 67 linewidth : int, 68 flush : unit -> unit } 69 of a string consumer, a specified linewidth, and a flush function 70 which is called whenever flush_ppstream is called. 71 72 A prettyprinter can be called outright to print a value. In 73 addition, a prettyprinter for a base type or nullary datatype ty 74 can be installed in the top-level system. Then the installed 75 prettyprinter will be invoked automatically whenever a value of 76 type ty is to be printed. 77 78 [break_style] is the type of line break styles for blocks: 79 80 [CONSISTENT] specifies that if any line break occurs inside the 81 block, then all indicated line breaks occur. 82 83 [INCONSISTENT] specifies that breaks will be inserted to only to 84 avoid overfull lines. 85 86 [mk_ppstream {consumer, linewidth, flush}] creates a new ppstream 87 which invokes the consumer to output text, putting at most 88 linewidth characters on each line. 89 90 [dest_ppstream ppstrm] extracts the linewidth, flush function, and 91 consumer from a ppstream. 92 93 [add_break ppstrm (size, offset)] notifies the pretty-printer that 94 a line break is possible at this point. 95 * When the current block style is CONSISTENT: 96 ** if the entire block fits on the remainder of the line, then 97 output size spaces; else 98 ** increase the current indentation by the block offset; 99 further indent every item of the block by offset, and add 100 one newline at every add_break in the block. 101 * When the current block style is INCONSISTENT: 102 ** if the next component of the block fits on the remainder of 103 the line, then output size spaces; else 104 ** issue a newline and indent to the current indentation level 105 plus the block offset plus the offset. 106 107 [add_newline ppstrm] issues a newline. 108 109 [add_stringsz ppstrm str] outputs the string str to the ppstream 110 (calculating its width using the UTF8.size function). 111 112 [add_string ppstrm (str,sz)] outputs the string str to the ppstream 113 but the ppstream treats it as if it were sz many characters wide 114 rather than its true width. 115 116 [begin_block ppstrm style blockoffset] begins a new block and 117 level of indentation, with the given style and block offset. 118 119 [end_block ppstrm] closes the current block. 120 121 [clear_ppstream ppstrm] restarts the stream, without affecting the 122 underlying consumer. 123 124 [flush_ppstream ppstrm] executes any remaining commands in the 125 ppstream (that is, flushes currently accumulated output to the 126 consumer associated with ppstrm); executes the flush function 127 associated with the consumer; and calls clear_ppstream. 128 129 [with_pp consumer f] makes a new ppstream from the consumer and 130 applies f (which can be thought of as a producer) to that 131 ppstream, then flushed the ppstream and returns the value of f. 132 133 [pp_to_string linewidth printit x] constructs a new ppstream 134 ppstrm whose consumer accumulates the output in a string s. Then 135 evaluates (printit ppstrm x) and finally returns the string s. 136*) 137end 138