From bbaf98addf32a6c2d0fe2919af965d2cded9976d Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 30 Oct 2021 16:16:42 -0400 Subject: [PATCH] fix: relax LSP spec compliance --- src/Lean/Server/Watchdog.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 55c316f8d3..48ee87e077 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -563,11 +563,15 @@ def initAndRunWatchdogAux : ServerM Unit := do discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams let clientTask ← runClientTask mainLoop clientTask - let Message.notification "exit" none ← st.hIn.readLspMessage - | throwServerError "Expected an exit notification" catch err => shutdown throw err + /- NOTE(WN): It looks like instead of sending the `exit` notification, + VSCode just closes the stream. In that case, pretend we got an `exit`. -/ + let Message.notification "exit" none ← + try st.hIn.readLspMessage + catch _ => pure (Message.notification "exit" none) + | throwServerError "Got `shutdown` request, expected an `exit` notification" def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do let mut workerPath ← IO.appPath