src/Pure/Thy/thy_parse.ML
changeset 5687 33ae54c0c821
parent 5248 6b04b9a88c21
child 5905 68cdba6c178f
equal deleted inserted replaced
5686:1f053d05f571 5687:33ae54c0c821
   228   !! (string -- (("[" $$-- nat --$$ "]") -- nat || nat >> (fn n => (n, n))))
   228   !! (string -- (("[" $$-- nat --$$ "]") -- nat || nat >> (fn n => (n, n))))
   229     >> (cat "Binder" o mk_triple2);
   229     >> (cat "Binder" o mk_triple2);
   230 
   230 
   231 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
   231 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
   232 
   232 
   233 val mixfix = string -- !! (opt_pris -- optional nat "max_pri")
   233 val mixfix = string -- !! (opt_pris -- optional nat "Syntax.max_pri")
   234   >> (cat "Mixfix" o mk_triple2);
   234   >> (cat "Mixfix" o mk_triple2);
   235 
   235 
   236 fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "NoSyn";
   236 fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "NoSyn";
   237 
   237 
   238 val opt_infix = opt_syn (infxl || infxr);
   238 val opt_infix = opt_syn (infxl || infxr);