From c8ee21747b1c44b80ba31626677295c02847b87f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 5 Jun 2020 10:03:25 +0200 Subject: [PATCH] chore: remove obsolete `symbolAux`, `symbolNoWsAux` --- src/Lean/Parser/Parser.lean | 5 +---- src/Lean/PrettyPrinter/Parenthesizer.lean | 6 +++--- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index a96bac9ade..7a089da969 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -1058,14 +1058,11 @@ fun c s => symbolNoWsFnAux sym ("'" ++ sym ++ "' without whitespace around it") /- Similar to `symbol`, but succeeds only if there is no space whitespace after leading term and after `sym`. -/ -@[inline] def symbolNoWsAux (sym : String) : Parser := +@[inline] def symbolNoWs (sym : String) : Parser := let sym := sym.trim; { info := symbolNoWsInfo sym, fn := symbolNoWsFn sym } -@[inline] def symbolNoWs (sym : String) : Parser := -symbolNoWsAux sym - def unicodeSymbolFnAux (sym asciiSym : String) (expected : List String) : ParserFn := satisfySymbolFn (fun s => s == sym || s == asciiSym) expected diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 34d9a037c9..a9ad9871c8 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -403,11 +403,11 @@ visitArgs $ do { } @[builtinParenthesizer symbol] -def symbolAux.parenthesizer : Parenthesizer | p => +def symbol.parenthesizer : Parenthesizer | p => evalOptPrec p.appArg! >>= visitToken -@[builtinParenthesizer symbolNoWsAux] def symbolNoWsAux.parenthesizer := symbolAux.parenthesizer -@[builtinParenthesizer unicodeSymbol] def unicodeSymbol.parenthesizer := symbolAux.parenthesizer +@[builtinParenthesizer symbolNoWs] def symbolNoWs.parenthesizer := symbol.parenthesizer +@[builtinParenthesizer unicodeSymbol] def unicodeSymbol.parenthesizer := symbol.parenthesizer @[builtinParenthesizer identNoAntiquot] def identNoAntiquot.parenthesizer : Parenthesizer | p => visitToken appPrec @[builtinParenthesizer rawIdent] def rawIdent.parenthesizer : Parenthesizer | p => visitToken appPrec