equal
deleted
inserted
replaced
210 (* mixfix annotations *) |
210 (* mixfix annotations *) |
211 |
211 |
212 val infxl = "infixl" $$-- !! nat >> cat "Infixl"; |
212 val infxl = "infixl" $$-- !! nat >> cat "Infixl"; |
213 val infxr = "infixr" $$-- !! nat >> cat "Infixr"; |
213 val infxr = "infixr" $$-- !! nat >> cat "Infixr"; |
214 |
214 |
215 fun mk_binder ((name, x), y) = |
215 val binder = "binder" $$-- |
216 let val (p1, p2) = if y = "None" then ("0", x) else (x, y); |
216 !! (string -- optional ("[" $$-- nat --$$ "]") "0" -- nat) |
217 in mk_triple (name, p1, p2) end; |
217 >> (cat "Binder" o mk_triple1); |
218 |
|
219 val binder = "binder" $$-- !! (string -- nat -- optional nat "None") |
|
220 >> (cat "Binder" o mk_binder); |
|
221 |
218 |
222 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list; |
219 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list; |
223 |
220 |
224 val mixfix = string -- !! (opt_pris -- optional nat "max_pri") |
221 val mixfix = string -- !! (opt_pris -- optional nat "max_pri") |
225 >> (cat "Mixfix" o mk_triple2); |
222 >> (cat "Mixfix" o mk_triple2); |