fix: changing whitespace after module header may break subsequent com…

…mands (#5312)

`with` considered harmful when merging old and new state, let's always
be explicit in these cases

src/Lean/Language/Lean.lean

@@ -322,16 +322,20 @@ 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
                 -- elaboration reuse
                 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

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

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": []}