From d75d7aa0d5de3dde20e9bc1f3341a5ff04e871f7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 8 Apr 2021 09:54:36 +0200
Subject: [PATCH] fix: server: ignore unknown implementation-dependent
 notifications

Fixes #383
---
 src/Lean/Server/Watchdog.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index b37230ef6f..e10edeabfb 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -416,7 +416,9 @@ section MessageHandling
     /- NOTE: textDocument/didChange is handled in the main loop. -/
     | "textDocument/didClose"  => handle DidCloseTextDocumentParams handleDidClose
     | "$/cancelRequest"        => handle CancelParams handleCancelRequest
-    | _                        => (←read).hLog.putStrLn s!"Got unsupported notification: {method}"
+    | _                        =>
+      if !"$/".isPrefixOf method then  -- implementation-dependent notifications can be safely ignored
+        (←read).hLog.putStrLn s!"Got unsupported notification: {method}"
 end MessageHandling
 
 section MainLoop