equal
deleted
inserted
replaced
398 (fixity_mixfix, []) => fixity_mixfix |
398 (fixity_mixfix, []) => fixity_mixfix |
399 | _ => Scan.!! (err s) Scan.fail () |
399 | _ => Scan.!! (err s) Scan.fail () |
400 end; |
400 end; |
401 |
401 |
402 val parse_fixity = |
402 val parse_fixity = |
403 (@{keyword "infix"} >> K X) || (@{keyword "infixl"} >> K L) || (@{keyword "infixr"} >> K R) |
403 (\<^keyword>\<open>infix\<close> >> K X) || (\<^keyword>\<open>infixl\<close> >> K L) || (\<^keyword>\<open>infixr\<close> >> K R) |
404 |
404 |
405 fun parse_mixfix x = |
405 fun parse_mixfix x = |
406 (Parse.string >> read_mixfix |
406 (Parse.string >> read_mixfix |
407 || parse_fixity -- Parse.nat -- Parse.string |
407 || parse_fixity -- Parse.nat -- Parse.string |
408 >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x; |
408 >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x; |