From 36bddc91cb05cb86c8a73eb127102b4aad5ce431 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Jun 2020 14:58:29 -0700
Subject: [PATCH] chore: remove `checkWsBeforeIfSymbol` hack

Now the `app` parsing rule always require some whitespace before the
first argument.

cc @Kha
---
 src/Lean/Parser/Parser.lean | 21 ---------------------
 src/Lean/Parser/Term.lean   |  2 +-
 2 files changed, 1 insertion(+), 22 deletions(-)

diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean
index 230e50f989..daaf8815f7 100644
--- a/src/Lean/Parser/Parser.lean
+++ b/src/Lean/Parser/Parser.lean
@@ -1078,27 +1078,6 @@ let sym := sym.trim;
 { info := symbolNoWsInfo sym,
   fn   := symbolNoWsFn sym }
 
-def checkWsBeforeIfSymbolFn (sym : String) (errorMsg : String) : ParserFn :=
-fun c s =>
-  let left := s.stxStack.back;
-  if checkTailNoWs left then
-    let iniSz  := s.stackSize;
-    let iniPos := s.pos;
-    let s := strAux sym "" 0 c s;
-    if s.hasError then
-      -- next token is not `sym`
-      s.restore iniSz iniPos
-    else
-      let s := s.restore iniSz iniPos;
-      s.mkError errorMsg
-  else
-    s -- there whitespace before `sym`
-
--- This parser fails if the next token is `sym`, but there is no space before it.
-def checkWsBeforeIfSymbol (sym : String) (errorMsg : String) : Parser :=
-{ info := epsilonInfo,
-  fn   := checkWsBeforeIfSymbolFn sym errorMsg }
-
 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 ae6f729e65..fac4808ce4 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -147,7 +147,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
 @[builtinTermParser] def uminus := parser!:65 "-" >> termParser 100
 
 def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
-@[builtinTermParser] def app      := tparser!:(maxPrec-1) checkWsBeforeIfSymbol "[" "expected space before '['" >> many1 (namedArgument <|> termParser maxPrec)
+@[builtinTermParser] def app      := tparser!:(maxPrec-1) checkWsBefore "expected space" >> many1 (namedArgument <|> termParser maxPrec)
 
 @[builtinTermParser] def proj     := tparser! symbolNoWs "." >> (fieldIdx <|> ident)
 @[builtinTermParser] def arrow    := tparser! unicodeInfixR " → " " -> " 25