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