feat: expand macros in syntax declaration

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)`,

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