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

chore: rename Parser.try to Parser.atomic

Browse source 
Reason: `try` is a keyword.

cc @Kha
This commit is contained in:
Leonardo de Moura 2020-11-17 08:25:01 -08:00
parent 178b3e5b52
commit 360fa1638f
9 changed files with 48 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -483,16 +483,16 @@ instance : OrElse Parser := ⟨orelse⟩
collectKinds := info.collectKinds
}
def tryFn (p : ParserFn) : ParserFn := fun c s =>
def atomicFn (p : ParserFn) : ParserFn := fun c s =>
let iniSz := s.stackSize
let iniPos := s.pos
match p c s with
| ⟨stack, _, cache, some msg⟩ => ⟨stack.shrink iniSz, iniPos, cache, some msg⟩
| other => other
@[inline] def «try» (p : Parser) : Parser := {
@[inline] def atomic (p : Parser) : Parser := {
info := p.info,
fn := tryFn p.fn
fn := atomicFn p.fn
}
def optionalFn (p : ParserFn) : ParserFn := fun c s =>
@ -1557,7 +1557,7 @@ def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true
-- antiquotation kind via `noImmediateColon`
let nameP := if anonymous then nameP <|> checkNoImmediateColon >> pushNone else nameP
-- antiquotations are not part of the "standard" syntax, so hide "expected '$'" on error
node kind $ «try» $
node kind $ atomic $
setExpected [] "$" >>
many (checkNoWsBefore "" >> "$") >>
checkNoWsBefore "no space before spliced term" >> antiquotExpr >>

22
src/Lean/Parser/Command.lean
View file

@ -45,15 +45,15 @@ def «constant» := parser! "constant " >> declId >> declSig >> optional d
def «instance» := parser! "instance " >> optional declId >> declSig >> declVal
def «axiom» := parser! "axiom " >> declId >> declSig
def «example» := parser! "example " >> declSig >> declVal
def inferMod := parser! «try» ("{" >> "}")
def inferMod := parser! atomic ("{" >> "}")
def ctor := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many ctor
def classInductive := parser! «try» ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
def structExplicitBinder := parser! «try» (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! «try» (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! «try» (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def classInductive := parser! atomic ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structFields := parser! many (ppLine >> (structExplicitBinder <|> structImplicitBinder <|> structInstBinder))
def structCtor := parser! «try» (declModifiers true >> ident >> optional inferMod >> " :: ")
def structCtor := parser! atomic (declModifiers true >> ident >> optional inferMod >> " :: ")
def structureTk := parser! "structure "
def classTk := parser! "class "
def «extends» := parser! " extends " >> sepBy1 termParser ", "
@ -80,16 +80,16 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "] " >> many1 ident
@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")"
def openHiding := parser! «try» (ident >> "hiding") >> many1 ident
def openHiding := parser! atomic (ident >> "hiding") >> many1 ident
def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident
def openRenaming := parser! «try» (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := parser! «try» (ident >> "(") >> many1 ident >> ")"
def openRenaming := parser! atomic (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := parser! atomic (ident >> "(") >> many1 ident >> ")"
def openSimple := parser! many1 ident
@[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notSymbol "end" >> commandParser) >> "end"
@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional («try» (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «builtin_initialize» := parser! "builtin_initialize " >> optional («try» (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «builtin_initialize» := parser! "builtin_initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «in» := tparser! " in " >> commandParser

10
src/Lean/Parser/Do.lean
View file

@ -28,13 +28,13 @@ def notFollowedByRedefinedTermToken :=
@[builtinDoElemParser] def doLet := parser! "let " >> optional "mut " >> letDecl
@[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doIdDecl := parser! «try» (ident >> optType >> leftArrow) >> doElemParser
def doPatDecl := parser! «try» (termParser >> leftArrow) >> doElemParser >> optional (" | " >> doElemParser)
def doIdDecl := parser! atomic (ident >> optType >> leftArrow) >> doElemParser
def doPatDecl := parser! atomic (termParser >> leftArrow) >> doElemParser >> optional (" | " >> doElemParser)
@[builtinDoElemParser] def doLetArrow := parser! "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
-- We use `letIdDeclNoBinders` to define `doReassign`.
-- Motivation: we do not reassign functions, and avoid parser conflict
def letIdDeclNoBinders := node `Lean.Parser.Term.letIdDecl $ «try» (ident >> pushNone >> optType >> " := ") >> termParser
def letIdDeclNoBinders := node `Lean.Parser.Term.letIdDecl $ atomic (ident >> pushNone >> optType >> " := ") >> termParser
@[builtinDoElemParser] def doReassign := parser! notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
@[builtinDoElemParser] def doReassignArrow := parser! notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
@ -68,7 +68,7 @@ else if c_2 then
action_3
```
-/
def elseIf := «try» (group (withPosition (" else " >> checkLineEq >> " if ")))
def elseIf := atomic (group (withPosition (" else " >> checkLineEq >> " if ")))
@[builtinDoElemParser] def doIf := parser! withPosition $
"if " >> optIdent >> termParser >> " then " >> doSeq
>> many (checkColGe "'else if' in 'do' must be indented" >> group (elseIf >> optIdent >> termParser >> " then " >> doSeq))
@ -81,7 +81,7 @@ def doMatchAlt : Parser := parser! sepBy1 termParser ", " >> darrow >> doSeq
def doMatchAlts : Parser := parser! withPosition $ (optional "| ") >> sepBy1 doMatchAlt (checkColGe "alternatives must be indented" >> "| ")
@[builtinDoElemParser] def doMatch := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
def doCatch := parser! «try» ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
def doCatch := parser! atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
def doCatchMatch := parser! "catch " >> doMatchAlts
def doFinally := parser! "finally " >> doSeq
@[builtinDoElemParser] def doTry := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally

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

@ -259,7 +259,7 @@ builtin_initialize
registerAlias "colGt" checkColGt
registerAlias "colGe" checkColGe
registerAlias "lookahead" lookahead
registerAlias "try" «try»
registerAlias "atomic" atomic
registerAlias "many" many
registerAlias "many1" many1
registerAlias "notFollowedBy" (notFollowedBy · "element")

16
src/Lean/Parser/Syntax.lean
View file

@ -22,7 +22,7 @@ builtin_initialize
def maxSymbol := parser! nonReservedSymbol "max" true
def precedenceLit : Parser := numLit <|> maxSymbol
def «precedence» := parser! ":" >> precedenceLit
def optPrecedence := optional («try» «precedence»)
def optPrecedence := optional (atomic «precedence»)
namespace Syntax
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@ -59,17 +59,17 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Par
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts)
def parserKind := parser! ident
def parserPrio := parser! numLit
def parserKindPrio := parser! «try» (ident >> ", ") >> numLit
def parserKindPrio := parser! atomic (ident >> ", ") >> numLit
def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|> parserPrio) >> "]")
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
def macroArg := «try» strLit <|> «try» macroArgSimple
def macroHead := macroArg <|> «try» ident
def macroTailTactic : Parser := «try» (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := «try» (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := «try» (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
def macroArg := strLit <|> atomic macroArgSimple
def macroHead := macroArg <|> ident
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
def optPrio := optional ("[" >> numLit >> "]")
@[builtinCommandParser] def «macro» := parser! suppressInsideQuot ("macro " >> optPrecedence >> optPrio >> macroHead >> many macroArg >> macroTail)
@ -77,7 +77,7 @@ def optPrio := optional ("[" >> numLit >> "]")
@[builtinCommandParser] def «elab_rules» := parser! suppressInsideQuot ("elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts)
def elabHead := macroHead
def elabArg := macroArg
def elabTail := «try» (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> termParser
def elabTail := atomic (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> termParser
@[builtinCommandParser] def «elab» := parser! suppressInsideQuot ("elab " >> optPrecedence >> optPrio >> elabHead >> many elabArg >> elabTail)
end Command

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

@ -31,7 +31,7 @@ def ident' : Parser := ident <|> "_"
@[builtinTacticParser] def «done» := parser! nonReservedSymbol "done"
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticSeq
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional («try» (ident >> " : ")) >> termParser 51 >> " = " >> ident
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional (atomic (ident >> " : ")) >> termParser 51 >> " = " >> ident
@[builtinTacticParser] def «unknown» := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
def locationWildcard := parser! "*"
@ -54,7 +54,7 @@ def withAlts : Parser := optional inductionAlts
def usingRec : Parser := optional (" using " >> ident)
def generalizingVars := optional (" generalizing " >> many1 ident)
@[builtinTacticParser] def «induction» := parser! nonReservedSymbol "induction " >> sepBy1 termParser ", " >> usingRec >> generalizingVars >> withAlts
def majorPremise := parser! optional («try» (ident >> " : ")) >> termParser
def majorPremise := parser! optional (atomic (ident >> " : ")) >> termParser
@[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> sepBy1 majorPremise ", " >> usingRec >> withAlts
def matchAlt : Parser := parser! sepBy1 termParser ", " >> darrow >> altRHS

22
src/Lean/Parser/Term.lean
View file

@ -59,7 +59,7 @@ def tupleTail := parser! ", " >> sepBy1 termParser ", "
def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
@[builtinTermParser] def paren := parser! "(" >> ppDedent (withoutPosition (withoutForbidden (optional (termParser >> parenSpecial)))) >> ")"
@[builtinTermParser] def anonymousCtor := parser! "⟨" >> sepBy termParser ", " >> "⟩"
def optIdent : Parser := optional («try» (ident >> " : "))
def optIdent : Parser := optional (atomic (ident >> " : "))
def fromTerm := parser! " from " >> termParser
def haveAssign := parser! " := " >> termParser
def haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
@ -70,14 +70,14 @@ def sufficesDecl := optIdent >> termParser >> (fromTerm <|> byTactic)
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
def structInstField := ppGroup $ parser! structInstLVal >> " := " >> termParser
@[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional («try» (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
@[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
def typeSpec := parser! " : " >> termParser
def optType : Parser := optional typeSpec
@[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec
@[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
def binderIdent : Parser := ident <|> hole
def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
def binderTactic := parser! «try» (" := " >> " by ") >> Tactic.tacticSeq
def binderTactic := parser! atomic (" := " >> " by ") >> Tactic.tacticSeq
def binderDefault := parser! " := " >> termParser
def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
@ -114,19 +114,19 @@ def matchAlts (optionalFirstBar := true) : Parser :=
ppLine >> (if optionalFirstBar then optional "| " else "| ") >>
sepBy1 (ppIndent matchAlt) (ppLine >> checkColGe "alternatives must be indented" >> "| ")
def matchDiscr := parser! optional («try» (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
def matchDiscr := parser! optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «nomatch» := parser!:leadPrec "nomatch " >> termParser
def funImplicitBinder := «try» (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder
def funSimpleBinder := «try» (lookahead (many1 binderIdent >> " : ")) >> simpleBinder
def funImplicitBinder := atomic (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder
def funSimpleBinder := atomic (lookahead (many1 binderIdent >> " : ")) >> simpleBinder
def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
-- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts false)
def optExprPrecedence := optional («try» ":" >> termParser maxPrec)
def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
@[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
@[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser
@[builtinTermParser] def borrowed := parser! "@&" >> termParser leadPrec
@ -138,8 +138,8 @@ def simpleBinderWithoutType := node `Lean.Parser.Term.simpleBinder (many1 binder
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
def letIdDecl := node `Lean.Parser.Term.letIdDecl $ «try» (letIdLhs >> " := ") >> termParser
def letPatDecl := node `Lean.Parser.Term.letPatDecl $ «try» (termParser >> pushNone >> optType >> " := ") >> termParser
def letIdDecl := node `Lean.Parser.Term.letIdDecl $ atomic (letIdLhs >> " := ") >> termParser
def letPatDecl := node `Lean.Parser.Term.letPatDecl $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser
def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false
-- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
@ -167,7 +167,7 @@ def «letrec» := parser!:leadPrec withPosition (group ("let " >> nonReservedSym
-- symbol precedence should be higher, but must match the one of `sub` below
@[builtinTermParser] def uminus := parser!:65 "-" >> termParser 100
def namedArgument := parser! «try» ("(" >> ident >> " := ") >> termParser >> ")"
def namedArgument := parser! atomic ("(" >> ident >> " := ") >> termParser >> ")"
def ellipsis := parser! ".."
@[builtinTermParser] def app := tparser!:(maxPrec-1) many1 $
checkWsBefore "expected space" >>
@ -185,7 +185,7 @@ def isIdent (stx : Syntax) : Bool :=
@[builtinTermParser] def explicitUniv : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
@[builtinTermParser] def namedPattern : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
@[builtinTermParser] def dollar := tparser!:0 «try» (" $" >> checkWsBefore "expected space") >> termParser 0
@[builtinTermParser] def dollar := tparser!:0 atomic (" $" >> checkWsBefore "expected space") >> termParser 0
@[builtinTermParser] def dollarProj := tparser!:0 " $. " >> (fieldIdx <|> ident)
@[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "

6
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -198,8 +198,8 @@ def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
def error.formatter (msg : String) : Formatter := pure ()
@[combinatorFormatter Lean.Parser.errorAtSavedPos]
def errorAtSavedPos.formatter (msg : String) (delta : Bool) : Formatter := pure ()
@[combinatorFormatter Lean.Parser.try]
def try.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.atomic]
def atomic.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.lookahead]
def lookahead.formatter (p : Formatter) : Formatter := pure ()
@ -422,7 +422,7 @@ builtin_initialize
registerAlias "colGt" checkColGt.formatter
registerAlias "colGe" checkColGe.formatter
registerAlias "lookahead" lookahead.formatter
registerAlias "try" try.formatter
registerAlias "atomic" atomic.formatter
registerAlias "many" many.formatter
registerAlias "many1" many1.formatter
registerAlias "notFollowedBy" notFollowedBy.formatter

6
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -338,8 +338,8 @@ def error.parenthesizer (msg : String) : Parenthesizer :=
def errorAtSavedPos.parenthesizer (msg : String) (delta : Bool) : Parenthesizer :=
pure ()
@[combinatorParenthesizer Lean.Parser.try]
def try.parenthesizer (p : Parenthesizer) : Parenthesizer :=
@[combinatorParenthesizer Lean.Parser.atomic]
def atomic.parenthesizer (p : Parenthesizer) : Parenthesizer :=
p
@[combinatorParenthesizer Lean.Parser.lookahead]
@ -501,7 +501,7 @@ builtin_initialize
registerAlias "colGt" checkColGt.parenthesizer
registerAlias "colGe" checkColGe.parenthesizer
registerAlias "lookahead" lookahead.parenthesizer
registerAlias "try" try.parenthesizer
registerAlias "atomic" atomic.parenthesizer
registerAlias "many" many.parenthesizer
registerAlias "many1" many1.parenthesizer
registerAlias "notFollowedBy" notFollowedBy.parenthesizer