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