max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: server: ignore unknown implementation-dependent notifications

Browse source 
Fixes #383
This commit is contained in:
Sebastian Ullrich 2021-04-08 09:54:36 +02:00
parent 898222686c
commit d75d7aa0d5
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Server/Watchdog.lean
View file

@ -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