From 37f5be1b264c02a235293af78e4fb7e402c4b30b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 6 Jan 2022 19:21:40 +0100
Subject: [PATCH] chore: fix servertest_init_exit

---
 src/Lean/Data/Lsp/Ipc.lean       | 3 +++
 tests/lean/server/init_exit.lean | 1 +
 2 files changed, 4 insertions(+)

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⟩