From 66777670e882edde86379fef6914b2938e93b51f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 27 May 2024 09:36:13 +0200
Subject: [PATCH] fix: stray tokens in tactic block should not inhibit
 incrementality (#4268)

---
 src/Lean/Parser/Command.lean                  | 35 ++++++++++++++++++-
 tests/lean/interactive/incrementalTactic.lean |  8 +++++
 .../incrementalTactic.lean.expected.out       |  1 +
 3 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index bd6645ba2eaf..e34a43da7e11 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -94,8 +94,41 @@ def declSig          := leading_parser
 /-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` -/
 def optDeclSig       := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
+/-- Right-hand side of a `:=` in a declaration, a term. -/
+def declBody : Parser :=
+  /-
+  We want to make sure that bodies starting with `by` in fact create a single `by` node instead of
+  accidentally parsing some remnants after it as well. This can especially happen when starting to
+  type comments inside tactic blocks where
+  ```
+  by
+    sleep 2000
+    unfold f
+    -starting comment here
+  ```
+  is parsed as
+  ```
+  (by
+    sleep 2000
+    unfold f
+    ) - (starting comment here)
+  ```
+  where the new nesting will discard incrementality data. By using `byTactic`'s precedence, the
+  stray `-` will be flagged as an unexpected token and will not disturb the syntax tree up to it. We
+  do not call `byTactic` directly to avoid differences in pretty printing or behavior or error
+  reporting between the two branches.
+  -/
+  lookahead (setExpected [] "by") >> termParser leadPrec <|>
+  termParser
+
+-- As the pretty printer ignores `lookahead`, we need a custom parenthesizer to choose the correct
+-- precedence
+open PrettyPrinter in
+@[combinator_parenthesizer declBody] def declBody.parenthesizer : Parenthesizer :=
+  Parenthesizer.categoryParser.parenthesizer `term 0
+
 def declValSimple    := leading_parser
-  " :=" >> ppHardLineUnlessUngrouped >> termParser >> Termination.suffix >> optional Term.whereDecls
+  " :=" >> ppHardLineUnlessUngrouped >> declBody >> Termination.suffix >> optional Term.whereDecls
 def declValEqns      := leading_parser
   Term.matchAltsWhereDecls
 def whereStructField := leading_parser
diff --git a/tests/lean/interactive/incrementalTactic.lean b/tests/lean/interactive/incrementalTactic.lean
index 73263d10f2c6..e5e153eeed1d 100644
--- a/tests/lean/interactive/incrementalTactic.lean
+++ b/tests/lean/interactive/incrementalTactic.lean
@@ -43,3 +43,11 @@ def otherMessage : Nat × Nat where
   fst := no
   snd := by skip
 --^ collectDiagnostics
+
+/-! Starting to type a comment should not invalidate the state above it. -/
+-- RESET
+def strayToken : True := by
+  dbg_trace "s"
+  unfold f
+        --^ sync
+        --^ insert: " -"
diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index 19f7534ae385..6b79256e2c12 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -53,3 +53,4 @@ t 2
    "fullRange":
    {"start": {"line": 3, "character": 9},
     "end": {"line": 3, "character": 16}}}]}
+s