From 96db4985eb4202ed183c6d6ac1fa40aa144a4cfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Nov 2020 10:48:22 -0800 Subject: [PATCH] feat: allow anonymous antiquotations at `ParserDescr.nodeWithAntiquot` --- src/Lean/Parser/Basic.lean | 4 ++-- src/Lean/Parser/Extension.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 3fb45d35e5..830957ae39 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1583,8 +1583,8 @@ def tryAnti (c : ParserContext) (s : ParserState) : Bool := /- End of Antiquotations -/ /- ===================== -/ -def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) : Parser := - withAntiquot (mkAntiquot name kind false) $ node kind p +def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anonymous := false) : Parser := + withAntiquot (mkAntiquot name kind anonymous) $ node kind p def ident : Parser := withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index a2f221d2ba..8e332c2deb 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -285,7 +285,7 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) | ParserDescr.unary n d => return (← getUnaryAlias parserAliasesRef n) (← visit d) | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parserAliasesRef n) (← visit d₁) (← visit d₂) | ParserDescr.node k prec d => return leadingNode k prec (← visit d) - | ParserDescr.nodeWithAntiquot n k d => return nodeWithAntiquot n k (← visit d) + | ParserDescr.nodeWithAntiquot n k d => return nodeWithAntiquot n k (← visit d) (anonymous := true) | ParserDescr.trailingNode k prec d => return trailingNode k prec (← visit d) | ParserDescr.symbol tk => return symbol tk | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol tk includeIdent