author | blanchet |
Thu, 16 Sep 2010 07:30:15 +0200 | |
changeset 39444 | beabb8443ee4 |
parent 39443 | e330437cd22a |
child 39501 | aaa7078fff55 |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* PRETTY-PRINTING *) |
|
39444 | 3 |
(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
signature Print = |
|
7 |
sig |
|
8 |
||
9 |
(* ------------------------------------------------------------------------- *) |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
10 |
(* Escaping strings. *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
11 |
(* ------------------------------------------------------------------------- *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
12 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
13 |
val escapeString : {escape : char list} -> string -> string |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
14 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
15 |
(* ------------------------------------------------------------------------- *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
16 |
(* A type of strings annotated with their size. *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
17 |
(* ------------------------------------------------------------------------- *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
18 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
19 |
type stringSize = string * int |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
20 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
21 |
val mkStringSize : string -> stringSize |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
22 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
23 |
(* ------------------------------------------------------------------------- *) |
39348 | 24 |
(* A type of pretty-printers. *) |
25 |
(* ------------------------------------------------------------------------- *) |
|
26 |
||
27 |
datatype breakStyle = Consistent | Inconsistent |
|
28 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
29 |
datatype step = |
39348 | 30 |
BeginBlock of breakStyle * int |
31 |
| EndBlock |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
32 |
| AddString of stringSize |
39348 | 33 |
| AddBreak of int |
34 |
| AddNewline |
|
35 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
36 |
type ppstream = step Stream.stream |
39348 | 37 |
|
38 |
(* ------------------------------------------------------------------------- *) |
|
39 |
(* Pretty-printer primitives. *) |
|
40 |
(* ------------------------------------------------------------------------- *) |
|
41 |
||
42 |
val beginBlock : breakStyle -> int -> ppstream |
|
43 |
||
44 |
val endBlock : ppstream |
|
45 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
46 |
val addString : stringSize -> ppstream |
39348 | 47 |
|
48 |
val addBreak : int -> ppstream |
|
49 |
||
50 |
val addNewline : ppstream |
|
51 |
||
52 |
val skip : ppstream |
|
53 |
||
54 |
val sequence : ppstream -> ppstream -> ppstream |
|
55 |
||
56 |
val duplicate : int -> ppstream -> ppstream |
|
57 |
||
58 |
val program : ppstream list -> ppstream |
|
59 |
||
60 |
val stream : ppstream Stream.stream -> ppstream |
|
61 |
||
62 |
val block : breakStyle -> int -> ppstream -> ppstream |
|
63 |
||
64 |
val blockProgram : breakStyle -> int -> ppstream list -> ppstream |
|
65 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
66 |
(* ------------------------------------------------------------------------- *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
67 |
(* Executing pretty-printers to generate lines. *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
68 |
(* ------------------------------------------------------------------------- *) |
39348 | 69 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
70 |
val execute : |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
71 |
{lineLength : int} -> ppstream -> |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
72 |
{indent : int, line : string} Stream.stream |
39348 | 73 |
|
74 |
(* ------------------------------------------------------------------------- *) |
|
75 |
(* Pretty-printer combinators. *) |
|
76 |
(* ------------------------------------------------------------------------- *) |
|
77 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
78 |
type 'a pp = 'a -> ppstream |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
79 |
|
39348 | 80 |
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp |
81 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
82 |
val ppString : string pp |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
83 |
|
39348 | 84 |
val ppBracket : string -> string -> 'a pp -> 'a pp |
85 |
||
86 |
val ppOp : string -> ppstream |
|
87 |
||
88 |
val ppOp2 : string -> 'a pp -> 'b pp -> ('a * 'b) pp |
|
89 |
||
90 |
val ppOp3 : string -> string -> 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp |
|
91 |
||
92 |
val ppOpList : string -> 'a pp -> 'a list pp |
|
93 |
||
94 |
val ppOpStream : string -> 'a pp -> 'a Stream.stream pp |
|
95 |
||
96 |
(* ------------------------------------------------------------------------- *) |
|
97 |
(* Pretty-printers for common types. *) |
|
98 |
(* ------------------------------------------------------------------------- *) |
|
99 |
||
100 |
val ppChar : char pp |
|
101 |
||
102 |
val ppEscapeString : {escape : char list} -> string pp |
|
103 |
||
104 |
val ppUnit : unit pp |
|
105 |
||
106 |
val ppBool : bool pp |
|
107 |
||
108 |
val ppInt : int pp |
|
109 |
||
110 |
val ppPrettyInt : int pp |
|
111 |
||
112 |
val ppReal : real pp |
|
113 |
||
114 |
val ppPercent : real pp |
|
115 |
||
116 |
val ppOrder : order pp |
|
117 |
||
118 |
val ppList : 'a pp -> 'a list pp |
|
119 |
||
120 |
val ppStream : 'a pp -> 'a Stream.stream pp |
|
121 |
||
122 |
val ppOption : 'a pp -> 'a option pp |
|
123 |
||
124 |
val ppPair : 'a pp -> 'b pp -> ('a * 'b) pp |
|
125 |
||
126 |
val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp |
|
127 |
||
128 |
val ppBreakStyle : breakStyle pp |
|
129 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
130 |
val ppStep : step pp |
39348 | 131 |
|
132 |
val ppPpstream : ppstream pp |
|
133 |
||
134 |
(* ------------------------------------------------------------------------- *) |
|
135 |
(* Pretty-printing infix operators. *) |
|
136 |
(* ------------------------------------------------------------------------- *) |
|
137 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
138 |
type token = string |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
139 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
140 |
datatype assoc = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
141 |
LeftAssoc |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
142 |
| NonAssoc |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
143 |
| RightAssoc |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
144 |
|
39348 | 145 |
datatype infixes = |
146 |
Infixes of |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
147 |
{token : token, |
39348 | 148 |
precedence : int, |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
149 |
assoc : assoc} list |
39348 | 150 |
|
151 |
val tokensInfixes : infixes -> StringSet.set |
|
152 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
153 |
val layerInfixes : infixes -> {tokens : StringSet.set, assoc : assoc} list |
39348 | 154 |
|
155 |
val ppInfixes : |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
156 |
infixes -> |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
157 |
('a -> (token * 'a * 'a) option) -> ('a * token) pp -> |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
158 |
('a * bool) pp -> ('a * bool) pp |
39348 | 159 |
|
160 |
(* ------------------------------------------------------------------------- *) |
|
161 |
(* Executing pretty-printers with a global line length. *) |
|
162 |
(* ------------------------------------------------------------------------- *) |
|
163 |
||
164 |
val lineLength : int ref |
|
165 |
||
166 |
val toString : 'a pp -> 'a -> string |
|
167 |
||
168 |
val toStream : 'a pp -> 'a -> string Stream.stream |
|
169 |
||
170 |
val trace : 'a pp -> string -> 'a -> unit |
|
171 |
||
172 |
end |