chore: rm ExprWithCtx

We will make this a separate PR

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

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`.