From 0602b805c8e7a8dfdfa714566e9eb118c4d7a2fc Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 11 Sep 2024 15:00:42 +0200
Subject: [PATCH] fix: changing whitespace after module header may break
 subsequent commands (#5312)

`with` considered harmful when merging old and new state, let's always
be explicit in these cases
---
 src/Lean/Language/Lean.lean                         | 10 +++++++---
 tests/lean/interactive/incrementalCommand.lean      | 13 +++++++++++++
 .../incrementalCommand.lean.expected.out            |  1 +
 3 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 3a2b936aa5..1db4988946 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -322,7 +322,8 @@ where
           stx := newStx
           diagnostics := old.diagnostics
           cancelTk? := ctx.newCancelTk
-          result? := some { oldSuccess with
+          result? := some {
+            parserState := newParserState
             processedSnap := (← oldSuccess.processedSnap.bindIO (sync := true) fun oldProcessed => do
               if let some oldProcSuccess := oldProcessed.result? then
                 -- also wait on old command parse snapshot as parsing is cheap and may allow for
@@ -330,8 +331,11 @@ where
                 oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
                   let prom ← IO.Promise.new
                   let _ ← IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState prom ctx)
-                  return .pure { oldProcessed with result? := some { oldProcSuccess with
-                    firstCmdSnap := { range? := none, task := prom.result } } }
+                  return .pure {
+                    diagnostics := oldProcessed.diagnostics
+                    result? := some {
+                      cmdState := oldProcSuccess.cmdState
+                      firstCmdSnap := { range? := none, task := prom.result } } }
               else
                 return .pure oldProcessed) } }
       else return old
diff --git a/tests/lean/interactive/incrementalCommand.lean b/tests/lean/interactive/incrementalCommand.lean
index e4cb72df76..cc6359e9bf 100644
--- a/tests/lean/interactive/incrementalCommand.lean
+++ b/tests/lean/interactive/incrementalCommand.lean
@@ -81,3 +81,16 @@ where
          --^ sync
          --^ insert: " "
          --^ collectDiagnostics
+
+/-!
+A reuse bug led to deletions after the header skipping a prefix of the next command on further edits
+-/
+-- RESET
+--asdf
+--^ delete: "a"
+--^ sync
+def f := 1  -- used to raise "unexpected identifier" after edit below because we would start parsing
+            -- on "ef"
+def g := 2
+   --^ insert: "g"
+   --^ collectDiagnostics
diff --git a/tests/lean/interactive/incrementalCommand.lean.expected.out b/tests/lean/interactive/incrementalCommand.lean.expected.out
index d397a33c33..da0491b780 100644
--- a/tests/lean/interactive/incrementalCommand.lean.expected.out
+++ b/tests/lean/interactive/incrementalCommand.lean.expected.out
@@ -33,3 +33,4 @@ w
    "message": "tactic 'assumption' failed\n⊢ False",
    "fullRange":
    {"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 9}}}]}
+{"version": 3, "uri": "file:///incrementalCommand.lean", "diagnostics": []}