equal
deleted
inserted
replaced
200 Scan.succeed []; |
200 Scan.succeed []; |
201 |
201 |
202 |
202 |
203 (* mixfix annotations *) |
203 (* mixfix annotations *) |
204 |
204 |
|
205 val infx = $$$ "infix" |-- !!! (nat >> Syntax.Infix || string -- nat >> Syntax.InfixName); |
205 val infxl = $$$ "infixl" |-- !!! (nat >> Syntax.Infixl || string -- nat >> Syntax.InfixlName); |
206 val infxl = $$$ "infixl" |-- !!! (nat >> Syntax.Infixl || string -- nat >> Syntax.InfixlName); |
206 val infxr = $$$ "infixr" |-- !!! (nat >> Syntax.Infixr || string -- nat >> Syntax.InfixrName); |
207 val infxr = $$$ "infixr" |-- !!! (nat >> Syntax.Infixr || string -- nat >> Syntax.InfixrName); |
207 |
208 |
208 val binder = |
209 val binder = |
209 $$$ "binder" |-- |
210 $$$ "binder" |-- |
218 >> (Syntax.Mixfix o triple2); |
219 >> (Syntax.Mixfix o triple2); |
219 |
220 |
220 fun opt_fix guard fix = |
221 fun opt_fix guard fix = |
221 Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn; |
222 Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn; |
222 |
223 |
223 val opt_infix = opt_fix !!! (infxl || infxr); |
224 val opt_infix = opt_fix !!! (infxl || infxr || infx); |
224 val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr); |
225 val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr || infx); |
225 |
226 |
226 val opt_infix' = opt_fix I (infxl || infxr); |
227 val opt_infix' = opt_fix I (infxl || infxr || infx); |
227 val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr); |
228 val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr || infx); |
228 |
229 |
229 |
230 |
230 (* consts *) |
231 (* consts *) |
231 |
232 |
232 val const = |
233 val const = |