From a3fe907a283cbaad4b184e3df6bdfad271ccd928 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Dec 2020 16:45:05 -0800
Subject: [PATCH] feat: add `attrParam` syntax category

cc @Kha
---
 src/Lean/Parser/Term.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index d013b1a1c5..3c68783daa 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -13,9 +13,16 @@ builtin_initialize
   registerBuiltinParserAttribute `builtinTacticParser `tactic (leadingIdentAsSymbol := true)
   registerBuiltinDynamicParserAttribute `tacticParser `tactic
 
+builtin_initialize
+  registerBuiltinParserAttribute `builtinAttrParamParser `attrParam (leadingIdentAsSymbol := true)
+  registerBuiltinDynamicParserAttribute `attrParamParser `attrParam
+
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=
   categoryParser `tactic rbp
 
+@[inline] def attrParamParser (rbp : Nat := 0) : Parser :=
+  categoryParser `attrParam rbp
+
 namespace Tactic
 
 def tacticSeq1Indented : Parser :=
@@ -202,6 +209,8 @@ def isIdent (stx : Syntax) : Bool :=
 @[builtinTermParser] def bracketedBinder.quot : Parser := parser! "`(bracketedBinder|"  >> toggleInsideQuot (evalInsideQuot ``bracketedBinder bracketedBinder) >> ")"
 @[builtinTermParser] def matchDiscr.quot : Parser := parser! "`(matchDiscr|"  >> toggleInsideQuot (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
 
+@[builtinTermParser] def attrParam.quot : Parser := parser! "`(attrParam|"  >> toggleInsideQuot attrParamParser >> ")"
+
 @[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
 @[builtinTermParser] def dbgTrace    := parser!:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser