From e021a7d0117238bb9baf30279cf2043ec5360cde Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 9 Oct 2020 16:17:56 -0700
Subject: [PATCH] chore: remove `symbolNoWs`

@Kha This is a leftover from the time precedence was associated with
tokens instead of parsers.
---
 src/Lean/Parser/Basic.lean                | 32 +----------------------
 src/Lean/Parser/Term.lean                 |  4 +--
 src/Lean/PrettyPrinter/Formatter.lean     |  1 -
 src/Lean/PrettyPrinter/Parenthesizer.lean |  1 -
 4 files changed, 3 insertions(+), 35 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index ce84798952..80dc4e016e 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1112,40 +1112,10 @@ fun c s =>
   let prev := pickNonNone s.stxStack;
   if checkTailNoWs prev then s else s.mkError errorMsg
 
-def checkNoWsBefore (errorMsg : String) : Parser :=
+def checkNoWsBefore (errorMsg : String := "no space") : Parser :=
 { info := epsilonInfo,
   fn   := checkNoWsBeforeFn errorMsg }
 
-def symbolNoWsInfo (sym : String) : ParserInfo :=
-{ collectTokens := fun tks => sym :: tks,
-  firstTokens   := FirstTokens.tokens [ sym ] }
-
-@[inline] def symbolNoWsFnAux (sym : String) (errorMsg : String) : ParserFn :=
-fun c s =>
-  let left := s.stxStack.back;
-  if checkTailNoWs left then
-    let startPos := s.pos;
-    let input    := c.input;
-    let s        := strAux sym errorMsg 0 c s;
-    if s.hasError then s
-    else
-      let leading   := mkEmptySubstringAt input startPos;
-      let stopPos   := startPos + sym.bsize;
-      let trailing  := mkEmptySubstringAt input stopPos;
-      let atom      := mkAtom { leading := leading, pos := startPos, trailing := trailing } sym;
-      s.pushSyntax atom
-  else
-    s.mkError errorMsg
-
-@[inline] def symbolNoWsFn (sym : String) : ParserFn :=
-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 symbolNoWs (sym : String) : Parser :=
-let sym := sym.trim;
-{ info := symbolNoWsInfo sym,
-  fn   := symbolNoWsFn sym }
-
 def unicodeSymbolFnAux (sym asciiSym : String) (expected : List String) : ParserFn :=
 satisfySymbolFn (fun s => s == sym || s == asciiSym) expected
 
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 78e445cbc3..eb623fd8f0 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -189,9 +189,9 @@ def ellipsis       := parser! ".."
   checkColGt "expected to be indented" >>
   (namedArgument <|> termParser maxPrec <|> ellipsis)
 
-@[builtinTermParser] def proj     := tparser! symbolNoWs "." >> (fieldIdx <|> ident)
+@[builtinTermParser] def proj     := tparser! checkNoWsBefore >> "." >> (fieldIdx <|> ident)
+@[builtinTermParser] def arrayRef := tparser! checkNoWsBefore >> "[" >> termParser >>"]"
 @[builtinTermParser] def arrow    := tparser! unicodeInfixR " → " " -> " 25
-@[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" >> termParser >>"]"
 
 def isIdent (stx : Syntax) : Bool :=
 -- antiquotations should also be allowed where an identifier is expected
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 4ce2fce075..8252b188c2 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -272,7 +272,6 @@ else do
   trace! `PrettyPrinter.format.backtrack ("unexpected syntax '" ++ stx ++ "', expected symbol '" ++ sym ++ "'");
   throwBacktrack
 
-@[combinatorFormatter symbolNoWs] def symbolNoWs.formatter := symbol.formatter
 @[combinatorFormatter nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
 
 @[combinatorFormatter unicodeSymbol]
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 4c143213ca..1766ca3a56 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -380,7 +380,6 @@ visitArgs $ do {
 }
 
 @[combinatorParenthesizer Lean.Parser.symbol] def symbol.parenthesizer := visitToken
-@[combinatorParenthesizer Lean.Parser.symbolNoWs] def symbolNoWs.parenthesizer := visitToken
 @[combinatorParenthesizer Lean.Parser.unicodeSymbol] def unicodeSymbol.parenthesizer := visitToken
 
 @[combinatorParenthesizer Lean.Parser.identNoAntiquot] def identNoAntiquot.parenthesizer := visitToken