src/Tools/Code/code_printer.ML
changeset 69593 3dda49e08b9d
parent 69485 b734ff28e405
child 69659 07025152dd80
equal deleted inserted replaced
69592:a80d8ec6c998 69593:3dda49e08b9d
   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;