equal
deleted
inserted
replaced
409 |
409 |
410 |
410 |
411 (* outer parser *) |
411 (* outer parser *) |
412 |
412 |
413 fun is_symid_meth s = |
413 fun is_symid_meth s = |
414 s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.ident_or_symbolic s; |
414 s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s; |
415 |
415 |
416 local |
416 local |
417 |
417 |
418 fun meth4 x = |
418 fun meth4 x = |
419 (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) || |
419 (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) || |