From c4c87ebe55d8fe6427232169032554d50e7cbdfd Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Fri, 15 Jul 2022 09:49:28 +0100
Subject: [PATCH] test: remove unused rpc case from runner

---
 tests/lean/interactive/run.lean | 23 -----------------------
 1 file changed, 23 deletions(-)

diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean
index 38a3ae0f68..22565a988c 100644
--- a/tests/lean/interactive/run.lean
+++ b/tests/lean/interactive/run.lean
@@ -81,7 +81,6 @@ partial def main (args : List String) : IO Unit := do
             IO.eprintln (toJson diag.param)
           requestNo := requestNo + 1
         | "widgets" =>
-          -- [todo] dedup with RPC
           if rpcSessionId.isNone then
             Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
             let r ← Ipc.readResponseAs requestNo RpcConnected
@@ -110,28 +109,6 @@ partial def main (args : List String) : IO Unit := do
             let resp ← Ipc.readResponseAs requestNo Lean.Widget.WidgetSource
             IO.eprintln (toJson resp.result)
             requestNo := requestNo + 1
-        | "RPC" =>
-          if rpcSessionId.isNone then
-            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
-            let r ← Ipc.readResponseAs requestNo RpcConnected
-            rpcSessionId := some r.result.sessionId
-            requestNo := requestNo + 1
-          let (method, params) ← liftExcept <| Except.mapError IO.userError <| Lean.Parsec.run (Prod.mk <$> ident <*> Json.Parser.any) params
-          let tdpp : TextDocumentPositionParams := {textDocument := { uri := uri}, position := pos}
-          -- hack for getWidgets which needs an explicit pos param.
-          let params := if method == `Lean.Widget.getWidgets then (toJson tdpp) else params
-          IO.eprintln (method, params)
-          let ps : RpcCallParams := {
-            textDocument := {uri := uri},
-            position := pos,
-            sessionId := rpcSessionId.get!,
-            method := method,
-            params := params,
-          }
-          Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
-          let response ← Ipc.readResponseAs requestNo Json
-          IO.eprintln response.result
-          requestNo := requestNo + 1
         | _ =>
           let Except.ok params ← pure <| Json.parse params
             | throw <| IO.userError s!"failed to parse {params}"