equal
deleted
inserted
replaced
4 Syntax extension. |
4 Syntax extension. |
5 *) |
5 *) |
6 |
6 |
7 signature SYNTAX_EXT = |
7 signature SYNTAX_EXT = |
8 sig |
8 sig |
9 val dddot_indexname: indexname |
|
10 datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T |
9 datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T |
11 val typ_to_nonterm: typ -> string |
10 val typ_to_nonterm: typ -> string |
12 datatype xsymb = |
11 datatype xsymb = |
13 Delim of string | |
12 Delim of string | |
14 Argument of string * int | |
13 Argument of string * int | |
54 end; |
53 end; |
55 |
54 |
56 structure Syntax_Ext: SYNTAX_EXT = |
55 structure Syntax_Ext: SYNTAX_EXT = |
57 struct |
56 struct |
58 |
57 |
59 |
|
60 (** misc definitions **) |
|
61 |
|
62 val dddot_indexname = ("dddot", 0); |
|
63 |
|
64 |
|
65 (** datatype xprod **) |
58 (** datatype xprod **) |
66 |
59 |
67 (*Delim s: delimiter s |
60 (*Delim s: delimiter s |
68 Argument (s, p): nonterminal s requiring priority >= p, or valued token |
61 Argument (s, p): nonterminal s requiring priority >= p, or valued token |
69 Space s: some white space for printing |
62 Space s: some white space for printing |