equal
deleted
inserted
replaced
4 Parsers for complex specifications. |
4 Parsers for complex specifications. |
5 *) |
5 *) |
6 |
6 |
7 signature SPEC_PARSE = |
7 signature SPEC_PARSE = |
8 sig |
8 sig |
9 type token = OuterParse.token |
|
10 type 'a parser = 'a OuterParse.parser |
|
11 val attrib: Attrib.src parser |
9 val attrib: Attrib.src parser |
12 val attribs: Attrib.src list parser |
10 val attribs: Attrib.src list parser |
13 val opt_attribs: Attrib.src list parser |
11 val opt_attribs: Attrib.src list parser |
14 val thm_name: string -> Attrib.binding parser |
12 val thm_name: string -> Attrib.binding parser |
15 val opt_thm_name: string -> Attrib.binding parser |
13 val opt_thm_name: string -> Attrib.binding parser |
34 |
32 |
35 structure SpecParse: SPEC_PARSE = |
33 structure SpecParse: SPEC_PARSE = |
36 struct |
34 struct |
37 |
35 |
38 structure P = OuterParse; |
36 structure P = OuterParse; |
39 type token = P.token; |
|
40 type 'a parser = 'a P.parser; |
|
41 |
37 |
42 |
38 |
43 (* theorem specifications *) |
39 (* theorem specifications *) |
44 |
40 |
45 val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src; |
41 val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src; |