From 8724a8cfd5e2a7f1902b55c30eb2f91eea88184d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Jun 2019 09:22:03 -0700
Subject: [PATCH] feat(library/init/lean/parser/parser): builtin parser
 attributes must be applied after compilation

---
 library/init/lean/parser/parser.lean |  4 +++-
 tests/playground/parser1.lean        | 24 ++++++------------------
 2 files changed, 9 insertions(+), 19 deletions(-)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index e0eb5e66ab..7dc4d49e07 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -1012,7 +1012,7 @@ def registerBuiltinParserAttribute (attrName : Name) (refDeclName : Name) : IO U
 registerAttribute {
  name  := attrName,
  descr := "Builtin parser",
- add   := λ env declName args persistent, do
+ add   := λ env declName args persistent, do {
    unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument")),
    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent")),
    match env.find declName with
@@ -1025,6 +1025,8 @@ registerAttribute {
        declareLeadingBuiltinParser env refDeclName declName
      | _ :=
        throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))
+ },
+ applicationTime := AttributeApplicationTime.afterCompilation
 }
 
 @[init mkBultinParsingTablesRef]
diff --git a/tests/playground/parser1.lean b/tests/playground/parser1.lean
index 3de0dfecc8..36e38ba95d 100644
--- a/tests/playground/parser1.lean
+++ b/tests/playground/parser1.lean
@@ -16,39 +16,27 @@ constant funKind : SyntaxNodeKind := default _
 
 local infixl `>>`:50 := Lean.Parser.andthen
 
-def pairParser : Parser :=
+@[builtinTestParser] def pairParser : Parser :=
 node pairKind $
   "(" >> number >> "," >> ident >> ")"
 
-attribute [builtinTestParser] pairParser
-
-def pairsParser : Parser :=
+@[builtinTestParser] def pairsParser : Parser :=
 node pairsKind $
   "{" >> sepBy1 testParser "," >> "}"
 
-attribute [builtinTestParser] pairsParser
-
-def functionParser : Parser :=
+@[builtinTestParser] def functionParser : Parser :=
 node funKind $
   "fun" >> ident >> "," >> testParser
 
-attribute [builtinTestParser] functionParser
-
-def identParser : Parser :=
+@[builtinTestParser] def identParser : Parser :=
 ident
 
-attribute [builtinTestParser] identParser
-
-def numParser : Parser :=
+@[builtinTestParser] def numParser : Parser :=
 number
 
-attribute [builtinTestParser] numParser
-
-def strParser : Parser :=
+@[builtinTestParser] def strParser : Parser :=
 strLit
 
-attribute [builtinTestParser] strParser
-
 def testParser (input : String) : IO Unit :=
 do
 env ← mkEmptyEnvironment,