diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index b38e8a5369..42c16638ef 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -57,34 +57,33 @@ structure InfoPopup where
 
 /-- Given elaborator info for a particular subexpression. Produce the `InfoPopup`.
 
-The intended usage of this is for the infoview to pass the `InfoWithCtx` which
+The intended usage of this is for the infoview to pass the `ExprWithCtx` which
 was stored for a particular `SubexprInfo` tag in a `TaggedText` generated with `ppExprTagged`.
  -/
-def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
+def makePopup : WithRpcRef ExprWithCtx → RequestM (RequestTask InfoPopup)
     | ⟨i⟩ => RequestM.asTask do
-      i.ctx.runMetaM i.info.lctx do
-        let type? ← match (← i.info.type?) with
-          | some type => some <$> ppExprTagged type
-          | none => pure none
-        let exprExplicit? ← match i.info with
-          | Elab.Info.ofTermInfo ti =>
-            let ti ← ppExprTagged ti.expr (explicit := true)
-            -- remove top-level expression highlight
-            pure <| some <| match ti with
-              | .tag _ tt => tt
-              | tt => tt
-          | Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString
-          | _ => pure none
+      i.ctx.runMetaM i.lctx do
+        let type? ←
+          (do return some <|← ppExprTagged <|← Meta.inferType i.expr)
+          <|> pure none
+        let ti ← ppExprTagged i.expr (explicit := true)
+        -- remove top-level expression highlight
+        let tt := match ti with
+          | .tag _ tt => tt
+          | tt => tt
+        let doc? ←
+          if let some n := i.expr.constName?
+          then findDocString? (← getEnv) n else pure none
         return {
           type := type?
-          exprExplicit := exprExplicit?
-          doc := ← i.info.docString? : InfoPopup
+          exprExplicit := some tt
+          doc := doc? : InfoPopup
         }
 
 builtin_initialize
   registerBuiltinRpcProcedure
     `Lean.Widget.InteractiveDiagnostics.infoToInteractive
-    (WithRpcRef InfoWithCtx)
+    (WithRpcRef ExprWithCtx)
     InfoPopup
     makePopup
 
@@ -132,23 +131,25 @@ builtin_initialize
 
 structure GetGoToLocationParams where
   kind : GoToKind
-  info : WithRpcRef InfoWithCtx
+  info : WithRpcRef ExprWithCtx
   deriving RpcEncoding
 
+def getGoToLocation : GetGoToLocationParams → RequestM (RequestTask (Array Lsp.LocationLink))
+  | ⟨kind, ⟨i⟩⟩ => RequestM.asTask do
+    let rc ← read
+    let ls ← FileWorker.locationLinksOfInfo kind i.ctx (ExprWithCtx.toTermInfo i)
+    if !ls.isEmpty then return ls
+    -- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications
+    let .app _ _ _ := i.expr | return #[]
+    let some nm := i.expr.getAppFn.constName? | return #[]
+    i.ctx.runMetaM i.lctx <|
+      locationLinksFromDecl rc.srcSearchPath rc.doc.meta.uri nm none
+
 builtin_initialize
   registerBuiltinRpcProcedure
     `Lean.Widget.getGoToLocation
     GetGoToLocationParams
     (Array Lsp.LocationLink)
-    fun ⟨kind, ⟨i⟩⟩ => RequestM.asTask do
-      let rc ← read
-      let ls ← FileWorker.locationLinksOfInfo kind i.ctx i.info
-      if !ls.isEmpty then return ls
-      -- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications
-      let .ofTermInfo ti := i.info | return #[]
-      let .app _ _ _ := ti.expr | return #[]
-      let some nm := ti.expr.getAppFn.constName? | return #[]
-      i.ctx.runMetaM ti.lctx <|
-        locationLinksFromDecl rc.srcSearchPath rc.doc.meta.uri nm none
+    getGoToLocation
 
 end Lean.Widget
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index dc93016dfa..d17104ea0c 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -6,38 +6,24 @@ 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.
--/
+/-- Expression with the context required to render it interactively in the infoview. -/
 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`.
-This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInteractive`.
-
-The purpose of `InfoWithCtx` is to carry over information about delaborated
-`Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
-functionality is purpose-specific to showing the contents of infoview popups.
--/
-structure InfoWithCtx where
-  ctx  : Elab.ContextInfo
-  info : Elab.Info
-  deriving Inhabited, RpcEncoding with { withRef := true }
-
 deriving instance RpcEncoding with { withRef := true } for MessageData
 
+/-- Creates a dummy Elab.Info from an ExprWithCtx. -/
+def ExprWithCtx.toTermInfo (e : ExprWithCtx) : Elab.Info :=
+  Elab.Info.ofTermInfo {
+    elaborator := Name.anonymous -- [todo] is this right?
+    stx := Syntax.missing -- [todo] is this right?
+    lctx := e.lctx
+    expr := e.expr
+    expectedType? := none
+  }
+
 instance : ToJson FVarId := ⟨fun f => toJson f.name⟩
 instance : ToJson MVarId := ⟨fun f => toJson f.name⟩
 instance : FromJson FVarId := ⟨fun j => FVarId.mk <$> fromJson? j⟩
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 965b34c11c..749f100d1c 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -17,8 +17,8 @@ open Server
 
 /-- Information about a subexpression within delaborated code. -/
 structure SubexprInfo where
-  /-- The `Elab.Info` node with the semantics of this part of the output. -/
-  info : WithRpcRef InfoWithCtx
+  /-- The Expression and context node with the semantics of this part of the output. -/
+  info : WithRpcRef ExprWithCtx
   /-- The position of this subexpression within the top-level expression.
   See `Lean.SubExpr`. -/
   subexprPos : Lean.SubExpr.Pos
@@ -40,8 +40,9 @@ where
   go (tt : TaggedText (Nat × Nat)) :=
     tt.rewrite fun (n, _) subTt =>
       match infos.find? n with
-      | none   => go subTt
-      | some i => TaggedText.tag ⟨WithRpcRef.mk { ctx, info := i }, n⟩ (go subTt)
+      | some (.ofTermInfo ti) => TaggedText.tag ⟨WithRpcRef.mk { ctx, lctx := ti.lctx, expr := ti.expr }, n⟩ (go subTt)
+      | some (.ofFieldInfo _fi) => go subTt -- [todo] what to do in this case?
+      | _ => go subTt
 
 def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
   let optsPerPos := if explicit then