From 3ee6aec4665e692fc191b677f98c8ce6b0da1d3e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Dec 2020 15:44:46 -0800
Subject: [PATCH] feat: add `attr` parser category

---
 src/Lean/Parser/Term.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 97c274287c..e21268e3be 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -21,6 +21,10 @@ builtin_initialize
   registerBuiltinParserAttribute `builtinAttrParamParser `attrParam
   registerBuiltinDynamicParserAttribute `attrParamParser `attrParam
 
+builtin_initialize
+  registerBuiltinParserAttribute `builtinAttrParser `attr
+  registerBuiltinDynamicParserAttribute `attrParser `attr
+
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=
   categoryParser `tactic rbp
 
@@ -30,6 +34,9 @@ builtin_initialize
 @[inline] def attrParamParser (rbp : Nat := 0) : Parser :=
   categoryParser `attrParam rbp
 
+@[inline] def attrParser (rbp : Nat := 0) : Parser :=
+  categoryParser `attr rbp
+
 namespace Tactic
 
 def tacticSeq1Indented : Parser :=
@@ -228,6 +235,7 @@ def isIdent (stx : Syntax) : Bool :=
 @[builtinTermParser] def matchDiscr.quot : Parser := parser! "`(matchDiscr|"  >> toggleInsideQuot (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
 
 @[builtinTermParser] def attrParam.quot : Parser := parser! "`(attrParam|"  >> toggleInsideQuot attrParamParser >> ")"
+@[builtinTermParser] def attr.quot : Parser := parser! "`(attr|"  >> toggleInsideQuot attrParser >> ")"
 
 @[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"