From 2edf02544ead0dc3bebffa1c533af4be5daeb928 Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Mon, 13 Jun 2022 17:14:18 -0400
Subject: [PATCH] chore: rm ExprWithCtx

We will make this a separate PR
---
 src/Lean/Server/FileWorker/WidgetRequests.lean | 15 ---------------
 src/Lean/Widget/Basic.lean                     | 16 ----------------
 2 files changed, 31 deletions(-)

diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index b38e8a5369..e708b4b2ae 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -17,21 +17,6 @@ import Lean.Server.FileWorker.RequestHandling
 namespace Lean.Widget
 open Server
 
-/-- Parameters for the `Lean.Widget.ppExprTagged` RPC.-/
-structure PPExprTaggedParams where
-  expr : WithRpcRef ExprWithCtx
-  explicit : Bool
-  deriving Inhabited, RpcEncoding
-
-builtin_initialize
-  registerBuiltinRpcProcedure
-    `Lean.Widget.ppExprTagged
-    PPExprTaggedParams
-    CodeWithInfos
-    fun ⟨⟨ctx, lctx, expr⟩, explicit⟩ => RequestM.asTask do
-      ctx.runMetaM lctx do
-        ppExprTagged expr explicit
-
 structure MsgToInteractive where
   msg : WithRpcRef MessageData
   indent : Nat
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index dc93016dfa..3ca433e116 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -6,22 +6,6 @@ namespace Lean.Widget
 
 open Elab Server
 
-/-- Expression with the context required to render it interactively in the infoview.
-
-The difference with `InfoWithCtx` is that this is an explicitly an expression which is not necessarily created during the elaboration step.
-
-The purpose of `ExprWithCtx` is so that widget writers can send an expression over and display it,
-as well as send it back in another RPC call for further processing.
-The former functionality can be achieved by sending `CodeWithInfos`, and even the latter could by inspecting the root tag for its `.ofTermInfo`.
-However `ExprWithCtx` gives a cleaner interface, and it gives the option to not pretty-print the expression,
-which can be useful if the widget code just needs it around as data, or wants to delay printing until the user requests it.
--/
-structure ExprWithCtx where
-  ctx  : Elab.ContextInfo
-  lctx : LocalContext
-  expr : Expr
-  deriving Inhabited, RpcEncoding with { withRef := true }
-
 /-- Elaborator information with elaborator context.
 
 This is used to tag different parts of expressions in `ppExprTagged`.