diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean index 570918d48f..21c880591f 100644 --- a/src/Lean/Data/Lsp/Ipc.lean +++ b/src/Lean/Data/Lsp/Ipc.lean @@ -42,6 +42,9 @@ def writeNotification (n : Notification α) : IpcM Unit := do def readMessage : IpcM JsonRpc.Message := do (←stdout).readLspMessage +def readRequestAs (expectedMethod : String) (α) [FromJson α] : IpcM (Request α) := do + (←stdout).readLspRequestAs expectedMethod α + def readResponseAs (expectedID : RequestID) (α) [FromJson α] : IpcM (Response α) := do (←stdout).readLspResponseAs expectedID α diff --git a/tests/lean/server/init_exit.lean b/tests/lean/server/init_exit.lean index d5addb231a..b421a2f68a 100644 --- a/tests/lean/server/init_exit.lean +++ b/tests/lean/server/init_exit.lean @@ -7,6 +7,7 @@ def main : IO Unit := do hIn.write (←FS.readBinFile "init_vscode_1_47_2.log") hIn.flush let initResp ← Ipc.readResponseAs 0 InitializeResult + let regWatchReq ← Ipc.readRequestAs "client/registerCapability" Json Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩ Ipc.writeRequest ⟨1, "shutdown", Json.null⟩