From 66a715dde110a60acf0464e39dcf34bd18ea2f3b Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sat, 2 Jan 2021 14:13:03 -0500
Subject: [PATCH] chore: tolerate more errors in server

---
 src/Lean/Server/FileWorker.lean |  7 ++++---
 src/Lean/Server/Watchdog.lean   | 10 +++++++---
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index ccc9f9506c..38308cf35d 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -225,9 +225,10 @@ section NotificationHandling
     let oldDoc ← (←read).docRef.get
     let some newVersion ← pure docId.version?
       | throwServerError "Expected version number"
-    if newVersion <= oldDoc.meta.version then
-      throwServerError "Got outdated version number"
-    if ¬ changes.isEmpty then
+    if newVersion ≤ oldDoc.meta.version then
+      -- TODO(WN): This happens on restart sometimes.
+      IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
+    else if ¬ changes.isEmpty then
       let (newDocText, minStartOff) := foldDocumentChanges changes oldDoc.meta.text
       updateDocument ⟨docId.uri, newVersion, newDocText⟩ minStartOff
     -- TODO(WN): cancel pending requests?
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 46dd0cc23f..7f6c6dc125 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -353,16 +353,20 @@ section MessageHandling
     | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam
     | "textDocument/hover"              => handle HoverParams
     | "textDocument/documentSymbol"     => handle DocumentSymbolParams
-    | _ => throwServerError s!"Got unsupported request: {method}"
+    | _                                 =>
+      (←read).hOut.writeLspResponseError
+        { id      := id
+          code    := ErrorCode.methodNotFound
+          message := s!"Unsupported request method: {method}" }
 
-  def handleNotification (method : String) (params : Json) : ServerM Unit :=
+  def handleNotification (method : String) (params : Json) : ServerM Unit := do
     let handle := (fun α [FromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler)
     match method with
     | "textDocument/didOpen"   => handle DidOpenTextDocumentParams handleDidOpen
     | "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange
     | "textDocument/didClose"  => handle DidCloseTextDocumentParams handleDidClose
     | "$/cancelRequest"        => handle CancelParams handleCancelRequest
-    | _                        => throwServerError "Got unsupported notification method"
+    | _                        => (←read).hLog.putStrLn s!"Got unsupported notification: {method}"
 end MessageHandling
 
 section MainLoop