chore: fix servertest_init_exit

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 α
 

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⟩