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