fix: Clear Diagnostics when file is closed

src/Lean/Data/Lsp/Communication.lean

@@ -117,6 +117,7 @@ section
 
   def writeLspResponseErrorWithData (h : FS.Stream) (e : ResponseError α) : IO Unit :=
     h.writeLspMessage e
+
 end
 
 end IO.FS.Stream

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⟩
+  while True do
+    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
 

src/Lean/Server/FileWorker.lean

@@ -422,6 +422,13 @@ section MessageHandling
 end MessageHandling
 
 section MainLoop
+
+  /-- called when document is closed so we can clear any diagnostics and cancel pending work -/
+  def exitWorker : WorkerM Unit := do
+    let state ← get
+    let doc := state.doc
+    doc.cancelTk.set
+
   partial def mainLoop : WorkerM Unit := do
     let ctx ← read
     let mut st ← get
@@ -450,8 +457,7 @@ section MainLoop
       handleRequest id method (toJson params)
       mainLoop
     | Message.notification "exit" none =>
-      let doc := (←get).doc
-      doc.cancelTk.set
+      exitWorker
       return ()
     | Message.notification method (some params) =>
       handleNotification method (toJson params)

src/Lean/Server/Watchdog.lean

@@ -307,6 +307,9 @@ section ServerM
   def terminateFileWorker (uri : DocumentUri) : ServerM Unit := do
     let fw ← findFileWorker! uri
     try
+      let ctx ← read
+      let meta := fw.doc.meta
+      publishDiagnostics meta #[] ctx.hOut
       fw.stdin.writeLspMessage (Message.notification "exit" none)
     catch _ =>
       /- The file worker must have crashed just when we were about to terminate it!

tests/lean/interactive/run.lean

@@ -127,8 +127,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

tests/lean/server/diags.lean

@@ -1,5 +1,8 @@
 import Lean.Data.Lsp
 open IO Lean Lsp
+open Lean
+open Lean.Lsp
+open Lean.JsonRpc
 
 def main : IO Unit := do
   Ipc.runWith (←IO.appPath) #["--server", "-Dlinter.all=false"] do
@@ -25,8 +28,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

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

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