equal
deleted
inserted
replaced
32 val is_proper: token -> bool |
32 val is_proper: token -> bool |
33 val mk_eof: Position.T -> token |
33 val mk_eof: Position.T -> token |
34 val eof: token |
34 val eof: token |
35 val is_eof: token -> bool |
35 val is_eof: token -> bool |
36 val stopper: token Scan.stopper |
36 val stopper: token Scan.stopper |
37 val idT: typ |
|
38 val longidT: typ |
|
39 val varT: typ |
|
40 val tidT: typ |
|
41 val tvarT: typ |
|
42 val terminals: string list |
37 val terminals: string list |
43 val is_terminal: string -> bool |
38 val is_terminal: string -> bool |
44 val literal_markup: string -> Markup.T |
39 val literal_markup: string -> Markup.T |
45 val report_of_token: token -> Position.report |
40 val report_of_token: token -> Position.report |
46 val reported_token_range: Proof.context -> token -> string |
41 val reported_token_range: Proof.context -> token -> string |
143 val stopper = Scan.stopper (K eof) is_eof; |
138 val stopper = Scan.stopper (K eof) is_eof; |
144 |
139 |
145 |
140 |
146 (* terminal arguments *) |
141 (* terminal arguments *) |
147 |
142 |
148 val idT = Type ("id", []); |
|
149 val longidT = Type ("longid", []); |
|
150 val varT = Type ("var", []); |
|
151 val tidT = Type ("tid", []); |
|
152 val tvarT = Type ("tvar", []); |
|
153 |
|
154 val terminal_kinds = |
143 val terminal_kinds = |
155 [("id", IdentSy), |
144 [("id", IdentSy), |
156 ("longid", LongIdentSy), |
145 ("longid", LongIdentSy), |
157 ("var", VarSy), |
146 ("var", VarSy), |
158 ("tid", TFreeSy), |
147 ("tid", TFreeSy), |