max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: allow anonymous antiquotations at ParserDescr.nodeWithAntiquot

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-17 10:48:22 -08:00
parent dfa0b97916
commit 96db4985eb
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Basic.lean
View file

@ -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

2
src/Lean/Parser/Extension.lean
View file

@ -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