diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 0e231ddfb8..7bba83d403 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -191,26 +191,31 @@ where return (stx, stackSz) processNullaryOrCat (stx : Syntax) := do - match (← elabParserName? stx[0]) with + let ident := stx[0] + let id := ident.getId.eraseMacroScopes + -- run when parser is neither a decl nor a cat + let default := do + if (← Parser.isParserAlias id) then + ensureNoPrec stx + return (← processAlias ident #[]) + throwError "unknown parser declaration/category/alias '{id}'" + match (← elabParserName? ident) with | some (.parser c (isDescr := true)) => ensureNoPrec stx -- `syntax _ :=` at least enforces this let stackSz := 1 return (mkIdentFrom stx c, stackSz) | some (.parser c (isDescr := false)) => + if (← Parser.getParserAliasInfo id).declName == c then + -- prefer parser alias over base declaration because it has more metadata, #2249 + return (← default) ensureNoPrec stx -- as usual, we assume that people using `Parser` know what they are doing let stackSz := 1 return (← `(ParserDescr.parser $(quote c)), stackSz) | some (.category _) => processParserCategory stx - | none => - let id := stx[0].getId.eraseMacroScopes - if (← Parser.isParserAlias id) then - ensureNoPrec stx - processAlias stx[0] #[] - else - throwError "unknown parser declaration/category/alias '{id}'" + | none => default processSepBy (stx : Syntax) := do let p ← ensureUnaryOutput <$> withNestedParser do process stx[1] diff --git a/tests/lean/run/2249.lean b/tests/lean/run/2249.lean new file mode 100644 index 0000000000..7599f37858 --- /dev/null +++ b/tests/lean/run/2249.lean @@ -0,0 +1,12 @@ +import Lean + +macro (name := fooParser) "foo" x:(ppSpace ident)* : term => + `([$(x.map (Lean.mkIdent ·.getId)),*]) + +namespace Lean.Parser.Term +macro (name := barParser) "bar" x:(ppSpace ident)* : term => + `([$(x.map (Lean.mkIdent ·.getId)),*]) + +variable (a : Nat) +#check foo a -- ok +#check bar a -- ok (used to be: unknown identifier '[anonymous]')