Longest match parser combinator or `<|>` variant

[leodemoura]

We currently use the longest match parser combinator only when processing syntax categories. During the ICERM after-party hackton, users created fake "syntax category" to get the longest match behavior. BTW, they were also confused by the following example:

syntax case1 := ident " : " term
syntax case2 := ident " ∈ " term 

syntax "foo " (case1 <|> case2) : term

#check foo x ∈ /- parser error at ∈ -/ Fin 10 

The problem is that <|> only backtracks if no token has been consumed. One has to use atomic here or hoist out the ident, but this is not natural to new users.