From 8a5344ed17d68283f3babd56f07c2aed969159e6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 16 Mar 2021 17:04:11 +0100
Subject: [PATCH] fix: server: handle requests for closed files

---
 src/Lean/Server/Watchdog.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index d2b6461331..0e3e2526f8 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -379,6 +379,17 @@ section MessageHandling
     let handle := fun α [FromJson α] [ToJson α] [FileSource α] => do
       let parsedParams ← parseParams α params
       let uri := fileSource parsedParams
+      try
+        findFileWorker uri
+      catch _ =>
+        -- VS Code sometimes sends us requests just after closing a file?
+        -- This is permitted by the spec, but seems pointless, and there's not much we can do,
+        -- so we return an error instead.
+        (←read).hOut.writeLspResponseError
+          { id      := id
+            code    := ErrorCode.contentModified
+            message := s!"Cannot process request to closed file '{uri}'" }
+        return
       tryWriteMessage uri ⟨id, method, parsedParams⟩ FileWorker.writeRequest
     match method with
     | "textDocument/waitForDiagnostics"   => handle WaitForDiagnosticsParams