From e6dec2dd79b29977aab4b7142515149a21ae01e1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Apr 2021 07:11:14 -0700
Subject: [PATCH] feat: don't allow whitespaces between `.` and field name

---
 src/Lean/Elab/App.lean      | 4 ++--
 src/Lean/Parser/Term.lean   | 4 ++--
 tests/lean/run/305.lean     | 2 +-
 tests/lean/run/KyleAlg.lean | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 506e4ebc6e..3e01af9a8d 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -812,9 +812,9 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     match f with
     | `($(e).$idx:fieldIdx) => elabFieldIdx e idx
-    | `($e |>. $idx:fieldIdx) => elabFieldIdx e idx
+    | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx
     | `($(e).$field:ident) => elabFieldName e field
-    | `($e |>. $field:ident) => elabFieldName e field
+    | `($e |>.$field:ident) => elabFieldName e field
     | `($e[%$bracket $idx]) => elabAppFn e (LVal.getOp bracket idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     | `($id:ident@$t:term) =>
       throwError "unexpected occurrence of named pattern"
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index f3d99cb276..25b283f8e3 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -203,7 +203,7 @@ def argument       :=
 -- argument precedence is `arg` (i.e. does not accept `lead` precedence)
 @[builtinTermParser] def app      := trailing_parser:leadPrec:maxPrec many1 argument
 
-@[builtinTermParser] def proj     := trailing_parser checkNoWsBefore >> "." >> (fieldIdx <|> ident)
+@[builtinTermParser] def proj     := trailing_parser checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> ident)
 @[builtinTermParser] def completion := trailing_parser checkNoWsBefore >> "."
 @[builtinTermParser] def arrayRef := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]"
 @[builtinTermParser] def arrow    := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
@@ -215,7 +215,7 @@ def isIdent (stx : Syntax) : Bool :=
 @[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
 @[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
 
-@[builtinTermParser] def pipeProj   := trailing_parser:minPrec " |>." >> (fieldIdx <|> ident) >> many argument
+@[builtinTermParser] def pipeProj   := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> ident) >> many argument
 @[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."
 
 @[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
diff --git a/tests/lean/run/305.lean b/tests/lean/run/305.lean
index fdd946eb86..970a6430a9 100644
--- a/tests/lean/run/305.lean
+++ b/tests/lean/run/305.lean
@@ -47,7 +47,7 @@ def readArgs : Id (Array Flag.Parsed) := panic! ""
 def parse (c : Cmd) : Id Cmd.Parsed := do
   let cmdName ← readSubCmds
   let flags ← readArgs
-  let cmd := c.subCmdByFullName? cmdName |>. get!
+  let cmd := c.subCmdByFullName? cmdName |>.get!
   let defaultedFlags : Array Flag.Parsed := #[]
   -- If we uncomment /-: Cmd.Parsed -/ two lines below or comment the line below, the elaborator stops hanging.
   let flags := defaultedFlags
diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean
index f29be419fd..7175640b21 100644
--- a/tests/lean/run/KyleAlg.lean
+++ b/tests/lean/run/KyleAlg.lean
@@ -225,7 +225,7 @@ def test8 {G : Type _} [Group G]: Group (G × G × G × G × G × G × G × G) :
 namespace Lean
 
 unsafe def Expr.dagSizeUnsafe (e : Expr) : IO Nat := do
-  let (_, s) ← visit e |>. run ({}, 0)
+  let (_, s) ← visit e |>.run ({}, 0)
   return s.2
 where
   visit (e : Expr) : StateRefT (Std.HashSet USize × Nat) IO Unit := do