feat: add prec syntax category

src/Lean/Parser/Syntax.lean

@@ -11,9 +11,14 @@ namespace Parser
 
 builtin_initialize
   registerBuiltinParserAttribute `builtinSyntaxParser `stx (leadingIdentAsSymbol := true)
+  registerBuiltinDynamicParserAttribute `stxParser `stx
 
 builtin_initialize
-  registerBuiltinDynamicParserAttribute `stxParser `stx
+  registerBuiltinParserAttribute `builtinPrecParser `prec (leadingIdentAsSymbol := true)
+  registerBuiltinDynamicParserAttribute `precParser `prec
+
+@[inline] def precedenceParser (rbp : Nat := 0) : Parser :=
+  categoryParser `prec rbp
 
 @[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
   categoryParser `stx rbp
@@ -39,6 +44,7 @@ end Syntax
 namespace Term
 
 @[builtinTermParser] def stx.quot : Parser := parser! "`(stx|"  >> toggleInsideQuot syntaxParser >> ")"
+@[builtinTermParser] def prec.quot : Parser := parser! "`(prec|"  >> toggleInsideQuot precedenceParser >> ")"
 
 end Term
 

src/Lean/Parser/Term.lean

@@ -151,10 +151,10 @@ def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
 @[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optSemicolon termParser
 @[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser
 def attrArg : Parser := ident <|> strLit <|> numLit
--- use `rawIdent` because of attribute names such as `instance`
 def «scoped» := parser! "scoped "
 def «local»  := parser! "local "
 def attrKind := parser! optional («scoped» <|> «local»)
+-- use `rawIdent` because of attribute names such as `instance`
 def attrInstance     := ppGroup $ parser! attrKind >> rawIdent >> many (ppSpace >> attrArg)
 
 def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"