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

chore: remove obsolete symbolAux, symbolNoWsAux

Browse source
This commit is contained in:
Sebastian Ullrich 2020-06-05 10:03:25 +02:00
parent 4250bc630e
commit c8ee21747b
2 changed files with 4 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Parser/Parser.lean
View file

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

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

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