diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean
index 29325d1a79..3a9d18af35 100644
--- a/src/Lean/Data/Lsp/Ipc.lean
+++ b/src/Lean/Data/Lsp/Ipc.lean
@@ -39,6 +39,23 @@ def writeRequest (r : Request α) : IpcM Unit := do
 def writeNotification (n : Notification α) : IpcM Unit := do
   (←stdin).writeLspNotification n
 
+def shutdown (requestNo : Nat) : IpcM Unit := do
+  let hIn ← stdout
+  let hOut ← stdin
+  hOut.writeLspRequest ⟨requestNo, "shutdown", Json.null⟩
+  repeat
+    let shutMsg ← hIn.readLspMessage
+    match shutMsg with
+    | Message.response id result =>
+      assert! result.isNull
+      if id != requestNo then
+        throw <| IO.userError s!"Expected id {requestNo}, got id {id}"
+
+      hOut.writeLspNotification ⟨"exit", Json.null⟩
+      break
+    | _ =>  -- ignore other messages in between.
+      pure ()
+
 def readMessage : IpcM JsonRpc.Message := do
   (←stdout).readLspMessage
 
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 9a3e28e341..2f746be6c7 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -449,7 +449,7 @@ section MainLoop
       handleRequest id method (toJson params)
       mainLoop
     | Message.notification "exit" none =>
-      let doc := (←get).doc
+      let doc := st.doc
       doc.cancelTk.set
       return ()
     | Message.notification method (some params) =>
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index b86d2009b6..278a9e409f 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -253,8 +253,11 @@ section ServerM
         if exitCode = 0 then
           -- Worker was terminated
           fw.errorPendingRequests o ErrorCode.contentModified
-            ("The file worker has been terminated. Either the header has changed,"
+            (s!"The file worker for {fw.doc.meta.uri} has been terminated. Either the header has changed,"
             ++ " or the file was closed, or the server is shutting down.")
+          -- one last message to clear the diagnostics for this file so that stale errors
+          -- do not remain in the editor forever.
+          publishDiagnostics fw.doc.meta #[] o
           return WorkerEvent.terminated
         else
           -- Worker crashed
diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean
index 99308137eb..6d71b44a47 100644
--- a/tests/lean/interactive/run.lean
+++ b/tests/lean/interactive/run.lean
@@ -178,8 +178,6 @@ partial def main (args : List String) : IO Unit := do
       | _ =>
         lastActualLineNo := lineNo
       lineNo := lineNo + 1
-    Ipc.writeRequest ⟨requestNo, "shutdown", Json.null⟩
-    let shutResp ← Ipc.readResponseAs requestNo Json
-    assert! shutResp.result.isNull
-    Ipc.writeNotification ⟨"exit", Json.null⟩
+
+    Ipc.shutdown requestNo
     discard <| Ipc.waitForExit
diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean
index 0f052c148b..7a17722756 100644
--- a/tests/lean/server/diags.lean
+++ b/tests/lean/server/diags.lean
@@ -25,8 +25,5 @@ def main : IO Unit := do
       else
         throw $ userError "Failed parsing test file."
 
-      Ipc.writeRequest ⟨2, "shutdown", Json.null⟩
-      let shutResp ← Ipc.readResponseAs 2 Json
-      assert! shutResp.result.isNull
-      Ipc.writeNotification ⟨"exit", Json.null⟩
+      Ipc.shutdown 2
       discard $ Ipc.waitForExit
diff --git a/tests/lean/server/edits.lean b/tests/lean/server/edits.lean
index a215e5d3e8..377e2306a2 100644
--- a/tests/lean/server/edits.lean
+++ b/tests/lean/server/edits.lean
@@ -30,8 +30,5 @@ def main : IO Unit := do
       else
         throw $ userError "Failed parsing test file."
 
-      Ipc.writeRequest ⟨3, "shutdown", Json.null⟩
-      let shutResp ← Ipc.readResponseAs 3 Json
-      assert! shutResp.result.isNull
-      Ipc.writeNotification ⟨"exit", Json.null⟩
+      Ipc.shutdown 3
       discard $ Ipc.waitForExit
diff --git a/tests/lean/server/init_exit.lean b/tests/lean/server/init_exit.lean
index b421a2f68a..1b2e8fa8e5 100644
--- a/tests/lean/server/init_exit.lean
+++ b/tests/lean/server/init_exit.lean
@@ -8,10 +8,7 @@ def main : IO Unit := do
     hIn.flush
     let initResp ← Ipc.readResponseAs 0 InitializeResult
     let regWatchReq ← Ipc.readRequestAs "client/registerCapability" Json
-    Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩ 
+    Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
 
-    Ipc.writeRequest ⟨1, "shutdown", Json.null⟩
-    let shutdownResp ← Ipc.readResponseAs 1 Json
-    assert! shutdownResp.result.isNull
-    Ipc.writeNotification ⟨"exit", Json.null⟩
+    Ipc.shutdown 1
     discard Ipc.waitForExit