fix: do not ban .. with a . on the next line (#4768)

Without this change, ```lean example : True := by refine' trivial .. . trivial ``` is a parse error.
leanprover · Sep 17, 2024 · b74f85a · b74f85a
1 parent 46b16b6
commit b74f85a
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
@@ -763,7 +763,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
@@ -0,0 +1,10 @@
+/-!
+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 ..
+  . trivial -- this has to be . not · for this test to be useful