equal
deleted
inserted
replaced
172 val name = group "name declaration" (short_ident || sym_ident || string || number); |
172 val name = group "name declaration" (short_ident || sym_ident || string || number); |
173 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number); |
173 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number); |
174 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim); |
174 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim); |
175 |
175 |
176 val uname = underscore >> K None || name >> Some; |
176 val uname = underscore >> K None || name >> Some; |
177 |
177 (* CB: underscore yields None, any other name Some with that string. |
|
178 Used, for example, in the renaming of locale parameters. *) |
178 |
179 |
179 (* sorts and arities *) |
180 (* sorts and arities *) |
180 |
181 |
181 val sort = group "sort" xname; |
182 val sort = group "sort" xname; |
182 |
183 |