chore: remove symbolNoWs

@Kha This is a leftover from the time precedence was associated with
tokens instead of parsers.

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
 

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

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]

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