From f876177f26e4940ffe4c577df5ec776ff5d77272 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Sep 2020 14:39:49 -0700
Subject: [PATCH] feat: expand macros in `syntax` declaration

---
 src/Lean/Elab/Syntax.lean   | 7 +++++--
 src/Lean/Parser/Syntax.lean | 3 +++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index f664410408..1ef3d55e09 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -158,8 +158,11 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
     d₁ ← withoutLeftRec $ toParserDescrAux (stx.getArg 0);
     d₂ ← withoutLeftRec $ toParserDescrAux (stx.getArg 2);
     `(ParserDescr.orelse $d₁ $d₂)
-  else
-    throwErrorAt stx $ "unexpected syntax kind of category `syntax`: " ++ kind
+  else do
+    stxNew? ← liftM (liftMacroM (expandMacro? stx) : TermElabM _);
+    match stxNew? with
+    | some stxNew => toParserDescrAux stxNew
+    | none => throwErrorAt stx $ "unexpected syntax kind of category `syntax`: " ++ kind
 
 /--
   Given a `stx` of category `syntax`, return a pair `(newStx, trailingParser)`,
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 99fde72723..7d75c7072f 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -13,6 +13,9 @@ namespace Parser
 let leadingIdentAsSymbol := true;
 registerBuiltinParserAttribute `builtinSyntaxParser `stx leadingIdentAsSymbol
 
+@[init] def regSyntaxParserAttribute : IO Unit :=
+registerBuiltinDynamicParserAttribute `stxParser `stx
+
 @[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
 categoryParser `stx rbp