From 360fa1638f70ebeb2b3d0824893e8050f440852e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Nov 2020 08:25:01 -0800 Subject: [PATCH] chore: rename `Parser.try` to `Parser.atomic` Reason: `try` is a keyword. cc @Kha --- src/Lean/Parser/Basic.lean | 8 ++++---- src/Lean/Parser/Command.lean | 22 +++++++++++----------- src/Lean/Parser/Do.lean | 10 +++++----- src/Lean/Parser/Extension.lean | 2 +- src/Lean/Parser/Syntax.lean | 16 ++++++++-------- src/Lean/Parser/Tactic.lean | 4 ++-- src/Lean/Parser/Term.lean | 22 +++++++++++----------- src/Lean/PrettyPrinter/Formatter.lean | 6 +++--- src/Lean/PrettyPrinter/Parenthesizer.lean | 6 +++--- 9 files changed, 48 insertions(+), 48 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index bffdad5272..3fb45d35e5 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -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 >> diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 17d9c8d0d2..ebe69761d3 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -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 diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index f9152d859d..4672464d0a 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -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 diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index d976d7a8d7..ba918c5aba 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -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") diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index febd427b2b..d9350691ab 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -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 diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index f3a8b28de6..3d238ca63d 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -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 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 93607dc7cd..07a2497d25 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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) " ▸ " diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index c5dce0b2c3..aea98a6c08 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -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 diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index dc2d956bfc..f406a8acd3 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -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