diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index 7ed471e345..b4c343f95e 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -17,6 +17,15 @@ import Lean.Server.FileWorker.RequestHandling
 namespace Lean.Widget
 open Server
 
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Lean.Widget.ppExprTagged
+    (WithRpcRef ExprWithCtx × Bool)
+    CodeWithInfos
+    fun (⟨ctx, lctx, expr⟩, explicit) => RequestM.asTask do
+      ctx.runMetaM lctx do
+        ppExprTagged expr explicit
+
 structure MsgToInteractive where
   msg : WithRpcRef MessageData
   indent : Nat
@@ -43,11 +52,11 @@ builtin_initialize
     fun ⟨i⟩ => RequestM.asTask do
       i.ctx.runMetaM i.info.lctx do
         let type? ← match (← i.info.type?) with
-          | some type => some <$> exprToInteractive type
+          | some type => some <$> ppExprTagged type
           | none => pure none
         let exprExplicit? ← match i.info with
           | Elab.Info.ofTermInfo ti =>
-            let ti ← exprToInteractive ti.expr (explicit := true)
+            let ti ← ppExprTagged ti.expr (explicit := true)
             -- remove top-level expression highlight
             pure <| some <| match ti with
               | .tag _ tt => tt
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index f1e45fed61..ffd7d233af 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -6,10 +6,17 @@ namespace Lean.Widget
 
 open Elab Server
 
-deriving instance RpcEncoding with { withRef := true } for Expr
-deriving instance RpcEncoding with { withRef := true } for LocalContext
-deriving instance RpcEncoding with { withRef := true } for ContextInfo
-deriving instance RpcEncoding with { withRef := true } for Info
+structure ExprWithCtx where
+  ctx  : Elab.ContextInfo
+  lctx : LocalContext
+  expr : Expr
+  deriving Inhabited, RpcEncoding with { withRef := true }
+
+structure InfoWithCtx where
+  ctx  : Elab.ContextInfo
+  info : Elab.Info
+  deriving Inhabited, RpcEncoding with { withRef := true }
+
 deriving instance RpcEncoding with { withRef := true } for MessageData
 
 end Lean.Widget
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 4ac494cad7..965b34c11c 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -7,6 +7,7 @@ Authors: Wojciech Nawrocki
 import Lean.PrettyPrinter
 import Lean.Server.Rpc.Basic
 import Lean.Widget.TaggedText
+import Lean.Widget.Basic
 
 /-! RPC infrastructure for storing and formatting code fragments, in particular `Expr`s,
 with environment and subexpression information. -/
@@ -14,13 +15,6 @@ with environment and subexpression information. -/
 namespace Lean.Widget
 open Server
 
--- TODO: Some of the `WithBlah` types exist mostly because we cannot derive multi-argument RPC wrappers.
--- They will be gone eventually.
-structure InfoWithCtx where
-  ctx : Elab.ContextInfo
-  info : Elab.Info
-  deriving Inhabited, RpcEncoding with { withRef := true }
-
 /-- Information about a subexpression within delaborated code. -/
 structure SubexprInfo where
   /-- The `Elab.Info` node with the semantics of this part of the output. -/
@@ -49,7 +43,7 @@ where
       | none   => go subTt
       | some i => TaggedText.tag ⟨WithRpcRef.mk { ctx, info := i }, n⟩ (go subTt)
 
-def exprToInteractive (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
+def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
   let optsPerPos := if explicit then
     Std.RBMap.ofList [
       (1, KVMap.empty.setBool `pp.all true),
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 6e47d35d68..6147157a03 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -75,8 +75,8 @@ open Meta in
 def addInteractiveHypothesis (hyps : Array InteractiveHypothesis) (ids : Array Name) (type : Expr) (value? : Option Expr := none) : MetaM (Array InteractiveHypothesis) := do
   return hyps.push {
     names      := ids.map toString
-    type       := (← exprToInteractive type)
-    val?       := (← value?.mapM exprToInteractive)
+    type       := (← ppExprTagged type)
+    val?       := (← value?.mapM ppExprTagged)
     isInstance := (← isClass? type).isSome
     isType     := (← instantiateMVars type).isSort
   }
@@ -133,7 +133,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
           ppVars varNames prevType? hyps localDecl
     let hyps ← pushPending varNames type? hyps
     let goalTp ← instantiateMVars mvarDecl.type
-    let goalFmt ← exprToInteractive goalTp
+    let goalFmt ← ppExprTagged goalTp
     let userName? := match mvarDecl.userName with
       | Name.anonymous => none
       | name           => some <| toString name.eraseMacroScopes