From bb66d4dd62bc686369f6253918afc376c44beb57 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 17 Jul 2024 02:16:03 +0100
Subject: [PATCH 1/3] fix: do not ban `..` with a `.` on the next line

Without this change,
```lean
example : True := by
  refine' trivial ..
  . trivial
```
is a parse error.
---
 src/Lean/Parser/Term.lean | 2 +-
 tests/lean/run/4768.lean  | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/4768.lean

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 0598cb401fbd..ae74e8639802 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -752,7 +752,7 @@ We use them to implement `macro_rules` and `elab_rules`
 def namedArgument  := leading_parser (withAnonymousAntiquot := false)
   atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")"
 def ellipsis       := leading_parser (withAnonymousAntiquot := false)
-  ".." >> notFollowedBy "." "`.` immediately after `..`"
+  ".." >> notFollowedBy (checkNoWsBefore >> ".") "`.` immediately after `..`"
 def argument       :=
   checkWsBefore "expected space" >>
   checkColGt "expected to be indented" >>
diff --git a/tests/lean/run/4768.lean b/tests/lean/run/4768.lean
new file mode 100644
index 000000000000..497431d5ff43
--- /dev/null
+++ b/tests/lean/run/4768.lean
@@ -0,0 +1,3 @@
+example : True := by
+  refine' trivial ..
+  . trivial

From e4f69395bff630a712c2cbb6c4e8236a2e02d9ec Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 5 Aug 2024 21:18:20 +0000
Subject: [PATCH 2/3] fix the test

---
 tests/lean/run/4768.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tests/lean/run/4768.lean b/tests/lean/run/4768.lean
index 497431d5ff43..da4793e67014 100644
--- a/tests/lean/run/4768.lean
+++ b/tests/lean/run/4768.lean
@@ -1,3 +1,4 @@
-example : True := by
-  refine' trivial ..
-  . trivial
+example : True ∧ True := by
+  constructor
+  refine trivial ..
+  . trivial -- this has to be . not · for this test to be useful

From 3d9bf22bcb715c8cedea36d6e59e89fdf5e3f676 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 29 Aug 2024 23:30:11 +0100
Subject: [PATCH 3/3] Add test docstring

---
 tests/lean/run/4768.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/tests/lean/run/4768.lean b/tests/lean/run/4768.lean
index da4793e67014..520f25caed2e 100644
--- a/tests/lean/run/4768.lean
+++ b/tests/lean/run/4768.lean
@@ -1,3 +1,9 @@
+/-!
+Test that `..` tokens do not break nearby `.`s.
+
+Note that this tests specifically for issues with `.` that are not present with `·`.
+-/
+
 example : True ∧ True := by
   constructor
   refine trivial ..