diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index 7e5712c3ad..2f84efe0f1 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -70,21 +70,23 @@ structure DiagnosticRelatedInformation where
   message : String
   deriving Inhabited, BEq, ToJson, FromJson
 
-structure Diagnostic where
+structure DiagnosticWith (α : Type) where
   range : Range
-  /-- extension: preserve semantic range of errors when truncating them for display purposes -/
+  /-- Extension: preserve semantic range of errors when truncating them for display purposes. -/
   fullRange : Range := range
   severity? : Option DiagnosticSeverity := none
   code? : Option DiagnosticCode := none
   source? : Option String := none
-  message : String
+  /-- Parametrised by the type of message data. LSP diagnostics use `String`,
+  whereas in Lean's interactive diagnostics we use the type of widget-enriched text.
+  See `Lean.Widget.InteractiveDiagnostic`. -/
+  message : α
   tags? : Option (Array DiagnosticTag) := none
   relatedInformation? : Option (Array DiagnosticRelatedInformation) := none
-  /-- Extension: interactive message widgets. We use untyped `Json` here due to dependency
-  ordering -- see `Lean.Widget.InteractiveDiagnostics`. -/
-  taggedMsg? : Option Json := none
   deriving Inhabited, BEq, ToJson, FromJson
 
+abbrev Diagnostic := DiagnosticWith String
+
 structure PublishDiagnosticsParams where
   uri : DocumentUri
   version? : Option Int := none
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 2a4795f5d9..5cd3770d2e 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -20,7 +20,7 @@ import Lean.Server.FileWorker.Utils
 import Lean.Server.FileWorker.RequestHandling
 import Lean.Server.Rpc.Basic
 
-import Lean.Widget.InteractiveDiagnostics
+import Lean.Widget.InteractiveDiagnostic
 
 /-!
 For general server architecture, see `README.md`. For details of IPC communication, see `Watchdog.lean`.
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index e90334d4f6..5bdd4ce5a1 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -208,7 +208,7 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
   let doc ← readDoc
   asTask do
     let ⟨cmdSnaps, e?⟩ ← doc.cmdSnaps.updateFinishedPrefix
-    let mut stxs := cmdSnaps.finishedPrefix.map Snapshot.stx
+    let mut stxs := cmdSnaps.finishedPrefix.map fun s => s.stx
     match e? with
     | some ElabTaskError.aborted =>
       throw RequestError.fileChanged
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
new file mode 100644
index 0000000000..ff241a5fe5
--- /dev/null
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
+import Lean.Widget.InteractiveCode
+import Lean.Widget.InteractiveGoal
+import Lean.Widget.InteractiveDiagnostic
+
+import Lean.Server.Rpc.RequestHandling
+
+/-! Registers all widget-related RPC procedures. -/
+
+namespace Lean.Widget
+open Server
+
+builtin_initialize
+  registerRpcCallHandler
+    `Lean.Widget.ExprWithCtx.tagged
+    (WithRpcRef ExprWithCtx)
+     CodeWithInfos
+    fun ⟨e⟩ => RequestM.asTask do e.ctx.runMetaM e.lctx (exprToInteractive e.expr)
+
+  registerRpcCallHandler
+    `Lean.Widget.ExprWithCtx.taggedExplicit
+    (WithRpcRef ExprWithCtx)
+    CodeWithInfos
+    fun ⟨e⟩ => RequestM.asTask do e.ctx.runMetaM e.lctx (exprToInteractiveExplicit e.expr)
+
+  registerRpcCallHandler
+    `Lean.Widget.ExprWithCtx.inferType
+    (WithRpcRef ExprWithCtx)
+    (WithRpcRef ExprWithCtx)
+    fun ⟨e⟩ => RequestM.asTask do WithRpcRef.mk <$> e.ctx.runMetaM e.lctx (inferType e.expr)
+
+structure MsgToInteractive where
+  msg : WithRpcRef MessageData
+  indent : Nat
+  deriving Inhabited, RpcEncoding
+
+builtin_initialize
+  registerRpcCallHandler
+    `Lean.Widget.InteractiveDiagnostics.msgToInteractive
+    MsgToInteractive
+    (TaggedText MsgEmbed)
+    fun ⟨⟨m⟩, i⟩ => RequestM.asTask do msgToInteractive m i
+
+structure InfoPopup where
+  type : Option CodeWithInfos
+  exprExplicit : Option CodeWithInfos
+  doc : Option String
+  deriving Inhabited, RpcEncoding
+
+builtin_initialize
+  registerRpcCallHandler
+    `Lean.Widget.InteractiveDiagnostics.infoToInteractive
+    (WithRpcRef InfoWithCtx)
+    InfoPopup
+    fun ⟨i⟩ => RequestM.asTask do
+      i.ctx.runMetaM i.lctx do
+        let type? ← match (← i.info.type?) with
+          | some type => some <$> exprToInteractive type
+          | none => none
+        let exprExplicit? ← match i.info with
+          | Elab.Info.ofTermInfo ti => some <$> exprToInteractiveExplicit ti.expr
+          | Elab.Info.ofFieldInfo fi => some (TaggedText.text fi.fieldName.toString)
+          | _ => none
+        return {
+          type := type?
+          exprExplicit := exprExplicit?
+          doc := ← i.info.docString? : InfoPopup
+        }
+
+open RequestM in
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask InteractiveGoals) := do
+  let doc ← readDoc
+  let text := doc.meta.text
+  let hoverPos := text.lspPosToUtf8Pos p.position
+  -- NOTE: use `>=` since the cursor can be *after* the input
+  withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
+    (notFoundX := return { goals := #[] }) fun snap => do
+      for t in snap.cmdState.infoState.trees do
+        if let rs@(_ :: _) := t.goalsAt? doc.meta.text hoverPos then
+          let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
+            let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
+            let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
+            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (goalToInteractive g))
+          return { goals := goals.toArray }
+
+      return { goals := #[] }
+
+open RequestM in
+partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
+    : RequestM (RequestTask (Option InteractiveGoal)) := do
+  let doc ← readDoc
+  let text := doc.meta.text
+  let hoverPos := text.lspPosToUtf8Pos p.position
+  withWaitFindSnap doc (fun s => s.endPos > hoverPos)
+    (notFoundX := pure none) fun snap => do
+      for t in snap.cmdState.infoState.trees do
+        if let some (ci, i@(Elab.Info.ofTermInfo ti)) := t.termGoalAt? hoverPos then
+         let ty ← ci.runMetaM i.lctx do
+           Meta.instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
+         -- for binders, hide the last hypothesis (the binder itself)
+         let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
+         let goal ← ci.runMetaM lctx' do
+           Meta.withPPInaccessibleNames <| goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
+         --let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
+         return some goal
+      return none
+
+builtin_initialize
+  registerRpcCallHandler
+    `Lean.Widget.getInteractiveGoals
+    Lsp.PlainGoalParams
+    InteractiveGoals
+    getInteractiveGoals
+
+  registerRpcCallHandler
+    `Lean.Widget.getInteractiveTermGoal
+    Lsp.PlainTermGoalParams
+    (Option InteractiveGoal)
+    getInteractiveTermGoal
+
+end Lean.Widget
diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index 866e0b7ece..78b249d081 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -142,7 +142,7 @@ instance [RpcEncoding α β] : RpcEncoding (Array α) (Array β) where
   rpcEncode a := a.mapM rpcEncode
   rpcDecode b := b.mapM rpcDecode
 
-instance [RpcEncoding α α'] [RpcEncoding β β']  : RpcEncoding (α × β) (α' × β') where
+instance [RpcEncoding α α'] [RpcEncoding β β'] : RpcEncoding (α × β) (α' × β') where
   rpcEncode := fun (a, b) => do
     let a' ← rpcEncode a
     let b' ← rpcEncode b
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 33b0d52bcb..3657ec252c 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -9,7 +9,7 @@ import Init.System.IO
 import Lean.Elab.Import
 import Lean.Elab.Command
 
-import Lean.Widget.InteractiveDiagnostics
+import Lean.Widget.InteractiveDiagnostic
 
 /-! One can think of this module as being a partial reimplementation
 of Lean.Elab.Frontend which also stores a snapshot of the world after
diff --git a/src/Lean/Widget.lean b/src/Lean/Widget.lean
index f835d22b4d..4345d487dd 100644
--- a/src/Lean/Widget.lean
+++ b/src/Lean/Widget.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Wojciech Nawrocki
 -/
-import Lean.Widget.Data
-import Lean.Widget.InteractiveGoals
-import Lean.Widget.InteractiveDiagnostics
+import Lean.Widget.InteractiveCode
+import Lean.Widget.InteractiveDiagnostic
+import Lean.Widget.InteractiveGoal
 import Lean.Widget.TaggedText
diff --git a/src/Lean/Widget/Data.lean b/src/Lean/Widget/Data.lean
deleted file mode 100644
index 718c68bc85..0000000000
--- a/src/Lean/Widget/Data.lean
+++ /dev/null
@@ -1,91 +0,0 @@
-import Lean.Elab.InfoTree
-import Lean.Server.Rpc.Basic
-import Lean.Widget.TaggedText
-
-/-! This file defines the widget RPC data types but few functions, since in general the UI may explore
-them in a mutually recursive fashion:
-msg -> trace -> goal -> expr -> info -> msg (only a subset of ctrs) -> ..
--/
-
-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
-  lctx : LocalContext
-  info : Elab.Info
-  deriving Inhabited, RpcEncoding with { withRef := true }
-
-/-- Pretty-printed syntax (usually but not necessarily an `Expr`) with embedded `Info`s. -/
-abbrev CodeWithInfos := TaggedText (WithRpcRef InfoWithCtx)
-
-def CodeWithInfos.pretty (tt : CodeWithInfos) :=
-  tt.stripTags
-
-structure InteractiveGoal where
-  hyps      : Array (String × CodeWithInfos)
-  type      : CodeWithInfos
-  userName? : Option String
-  deriving Inhabited, RpcEncoding
-
-namespace InteractiveGoal
-
-def pretty (g : InteractiveGoal) : String :=
-  let ret := match g.userName? with
-    | some userName => s!"case {userName}\n"
-    | none          => ""
-  let hyps := g.hyps.map fun (name, tt) => s!"{name} : {tt.stripTags}"
-  let ret := ret ++ "\n".intercalate hyps.toList
-  ret ++ s!"⊢ {g.type.stripTags}"
-
-end InteractiveGoal
-
-deriving instance RpcEncoding with { withRef := true } for MessageData
-
-inductive MsgEmbed where
-  | expr : CodeWithInfos → MsgEmbed
-  | goal : InteractiveGoal → MsgEmbed
-  | lazyTrace : Nat → Name → WithRpcRef MessageData → MsgEmbed
-  deriving Inhabited
-
-namespace MsgEmbed
-
--- TODO(WN): `deriving RpcEncoding` for `inductive`
-private inductive RpcEncodingPacket where
-  | expr : TaggedText Lsp.RpcRef → RpcEncodingPacket
-  | goal : Nat → RpcEncodingPacket -- TODO
-  | lazyTrace : Nat → Name → Lsp.RpcRef → RpcEncodingPacket
-  deriving Inhabited, FromJson, ToJson
-
-instance : RpcEncoding MsgEmbed RpcEncodingPacket where
-  rpcEncode a := match a with
-    | expr t            => return RpcEncodingPacket.expr (← rpcEncode t)
-    | goal t            => return RpcEncodingPacket.goal 0
-    | lazyTrace col n t => return RpcEncodingPacket.lazyTrace col n (← rpcEncode t)
-
-  rpcDecode a := match a with
-    | RpcEncodingPacket.expr t            => return expr (← rpcDecode t)
-    | RpcEncodingPacket.goal t            => return unreachable!
-    | RpcEncodingPacket.lazyTrace col n t => return lazyTrace col n (← rpcDecode t)
-
-end MsgEmbed
-
-/-- We embed objects in messages by storing them in the tag of an empty subtree (`text ""`).
-In other words, we terminate the `MsgEmbed`-tagged tree at embedded objects and instead
-store the pretty-printed embed (which can itself be a `TaggedText`) in the tag. -/
-abbrev InteractiveMessage := TaggedText MsgEmbed
-
-namespace InteractiveMessage
-open MsgEmbed
-
-def pretty (msg : InteractiveMessage) : String :=
-  let tt : TaggedText MsgEmbed := msg.rewrite fun
-    | expr tt,         _     => TaggedText.text tt.stripTags
-    | goal g,          _     => TaggedText.text g.pretty
-    | lazyTrace _ _ _, subTt => subTt
-  tt.stripTags
-
-end InteractiveMessage
-end Lean.Widget
diff --git a/src/Lean/Widget/ExprWithCtx.lean b/src/Lean/Widget/InteractiveCode.lean
similarity index 79%
rename from src/Lean/Widget/ExprWithCtx.lean
rename to src/Lean/Widget/InteractiveCode.lean
index d467129586..784d0c46ff 100644
--- a/src/Lean/Widget/ExprWithCtx.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -6,23 +6,34 @@ Authors: Wojciech Nawrocki
 -/
 import Lean.PrettyPrinter
 import Lean.Server.Rpc.Basic
-import Lean.Server.Rpc.RequestHandling
 import Lean.Widget.TaggedText
-import Lean.Widget.Data
 
-/-! RPC infrastructure for storing/formatting `Expr`s with environment and subexpression information. -/
+/-! RPC infrastructure for storing and formatting code fragments, in particular `Expr`s,
+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
+  lctx : LocalContext
+  info : Elab.Info
+  deriving Inhabited, RpcEncoding with { withRef := true }
+
+/-- Pretty-printed syntax (usually but not necessarily an `Expr`) with embedded `Info`s. -/
+abbrev CodeWithInfos := TaggedText (WithRpcRef InfoWithCtx)
+
+def CodeWithInfos.pretty (tt : CodeWithInfos) :=
+  tt.stripTags
+
 structure ExprWithCtx where
   ctx : Elab.ContextInfo
   lctx : LocalContext
   expr : Expr
   deriving Inhabited, RpcEncoding with { withRef := true }
 
-namespace ExprWithCtx
-
 open Expr in
 /-- Find a subexpression of `e` using the pretty-printer address scheme. -/
 -- NOTE(WN): not currently in use
@@ -61,7 +72,7 @@ where
         | 0, proj _ _ e₁ _ => go' e₁
         | _, _             => (lctx, e) -- panic! s!"cannot descend {a} into {e.expr}"
 
--- TODO(WN): should these go in `Lean.PrettyPrinter` ?
+-- TODO(WN): should the two fns below go in `Lean.PrettyPrinter` ?
 open PrettyPrinter in
 private def formatWithOpts (e : Expr) (optsPerPos : Delaborator.OptionsPerPos)
     : MetaM (Format × Std.RBMap Nat Elab.Info compare) := do
@@ -78,8 +89,8 @@ private def formatWithOpts (e : Expr) (optsPerPos : Delaborator.OptionsPerPos)
 def formatInfos (e : Expr) : MetaM (Format × Std.RBMap Nat Elab.Info compare) :=
   formatWithOpts e {}
 
-/-- Like `formatM` but with `pp.all` set at the top-level expression. -/
-def formatExplicitInfos (e : Expr) : MetaM (Format × Std.RBMap Nat Elab.Info compare) := do
+/-- Like `formatInfos` but with `pp.all` set at the top-level expression. -/
+def formatExplicitInfos (e : Expr) : MetaM (Format × Std.RBMap Nat Elab.Info compare) :=
   let optsPerPos := Std.RBMap.ofList [(1, KVMap.empty.setBool `pp.all true)]
   formatWithOpts e optsPerPos
 
@@ -105,7 +116,7 @@ def inferType (e : Expr) : MetaM ExprWithCtx := do
   }
   return { ctx, lctx := ← getLCtx, expr := e}
 
-def tagged (e : Expr) : MetaM CodeWithInfos := do
+def exprToInteractive (e : Expr) : MetaM CodeWithInfos := do
   let (fmt, infos) ← formatInfos e
   let tt := TaggedText.prettyTagged fmt
   let ctx := {
@@ -118,7 +129,7 @@ def tagged (e : Expr) : MetaM CodeWithInfos := do
   }
   tagExprInfos ctx (← getLCtx) infos tt
 
-def taggedExplicit (e : Expr) : MetaM CodeWithInfos := do
+def exprToInteractiveExplicit (e : Expr) : MetaM CodeWithInfos := do
   let (fmt, infos) ← formatExplicitInfos e
   let tt := TaggedText.prettyTagged fmt
   let ctx := {
@@ -131,10 +142,4 @@ def taggedExplicit (e : Expr) : MetaM CodeWithInfos := do
   }
   tagExprInfos ctx (← getLCtx) infos tt
 
-builtin_initialize
-  registerRpcCallHandler `Lean.Widget.ExprWithCtx.tagged         (WithRpcRef ExprWithCtx) CodeWithInfos            fun ⟨e⟩ => RequestM.asTask do e.ctx.runMetaM e.lctx (tagged e.expr)
-  registerRpcCallHandler `Lean.Widget.ExprWithCtx.taggedExplicit (WithRpcRef ExprWithCtx) CodeWithInfos            fun ⟨e⟩ => RequestM.asTask do e.ctx.runMetaM e.lctx (taggedExplicit e.expr)
-  registerRpcCallHandler `Lean.Widget.ExprWithCtx.inferType      (WithRpcRef ExprWithCtx) (WithRpcRef ExprWithCtx) fun ⟨e⟩ => RequestM.asTask do WithRpcRef.mk <$> e.ctx.runMetaM e.lctx (inferType e.expr)
-
-end ExprWithCtx
 end Lean.Widget
diff --git a/src/Lean/Widget/InteractiveDiagnostics.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
similarity index 71%
rename from src/Lean/Widget/InteractiveDiagnostics.lean
rename to src/Lean/Widget/InteractiveDiagnostic.lean
index cdd87e951c..73d1acf527 100644
--- a/src/Lean/Widget/InteractiveDiagnostics.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -8,15 +8,71 @@ import Lean.Data.Lsp
 import Lean.Message
 import Lean.Elab.InfoTree
 import Lean.PrettyPrinter
+
 import Lean.Server.Utils
 import Lean.Server.Rpc.Basic
+
 import Lean.Widget.TaggedText
-import Lean.Widget.Data
-import Lean.Widget.ExprWithCtx
+import Lean.Widget.InteractiveCode
+import Lean.Widget.InteractiveGoal
 
 namespace Lean.Widget
 open Lsp Server
 
+deriving instance RpcEncoding with { withRef := true } for MessageData
+
+inductive MsgEmbed where
+  | expr : CodeWithInfos → MsgEmbed
+  | goal : InteractiveGoal → MsgEmbed
+  | lazyTrace : Nat → Name → WithRpcRef MessageData → MsgEmbed
+  deriving Inhabited
+
+namespace MsgEmbed
+
+-- TODO(WN): `deriving RpcEncoding` for `inductive`
+private inductive RpcEncodingPacket where
+  | expr : TaggedText Lsp.RpcRef → RpcEncodingPacket
+  | goal : Nat → RpcEncodingPacket -- TODO
+  | lazyTrace : Nat → Name → Lsp.RpcRef → RpcEncodingPacket
+  deriving Inhabited, FromJson, ToJson
+
+instance : RpcEncoding MsgEmbed RpcEncodingPacket where
+  rpcEncode a := match a with
+    | expr t            => return RpcEncodingPacket.expr (← rpcEncode t)
+    | goal t            => return RpcEncodingPacket.goal 0
+    | lazyTrace col n t => return RpcEncodingPacket.lazyTrace col n (← rpcEncode t)
+
+  rpcDecode a := match a with
+    | RpcEncodingPacket.expr t            => return expr (← rpcDecode t)
+    | RpcEncodingPacket.goal t            => return unreachable!
+    | RpcEncodingPacket.lazyTrace col n t => return lazyTrace col n (← rpcDecode t)
+
+end MsgEmbed
+
+/-- A `Lean.Message` with support for interactive elements. -/
+structure InteractiveMessage extends Message where
+  interactiveMsg : TaggedText MsgEmbed
+
+/-- We embed objects in LSP diagnostics by storing them in the tag of an empty subtree (`text ""`).
+In other words, we terminate the `MsgEmbed`-tagged tree at embedded objects and instead store
+the pretty-printed embed (which can itself be a `TaggedText`) in the tag. -/
+abbrev InteractiveDiagnostic := Lsp.DiagnosticWith (TaggedText MsgEmbed)
+
+namespace InteractiveDiagnostic
+open MsgEmbed
+
+def toDiagnostic (diag : InteractiveDiagnostic) : Lsp.Diagnostic :=
+  { diag with message := prettyTt diag.message }
+where
+  prettyTt (tt : TaggedText MsgEmbed) : String :=
+    let tt : TaggedText MsgEmbed := tt.rewrite fun
+      | expr tt,         _     => TaggedText.text tt.stripTags
+      | goal g,          _     => TaggedText.text g.pretty
+      | lazyTrace _ _ _, subTt => subTt
+    tt.stripTags
+
+end InteractiveDiagnostic
+
 private def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := {
   env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts,
   currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls
@@ -65,7 +121,7 @@ where
       currNamespace := nCtx.currNamespace
       openDecls := nCtx.openDecls
     }
-    let (fmt, infos) ← ci.runMetaM ctx.lctx (ExprWithCtx.formatInfos e)
+    let (fmt, infos) ← ci.runMetaM ctx.lctx (formatInfos e)
     let t ← pushEmbed <| EmbedFmt.expr ci ctx.lctx infos
     return Format.tag t fmt
   | _,    none,      ofGoal mvarId            => pure $ "goal " ++ format (mkMVar mvarId)
@@ -97,7 +153,7 @@ partial def msgToInteractive (msgData : MessageData) (indent : Nat := 0) : IO (T
   tt.rewriteM fun (n, col) subTt =>
     match embeds.get! n with
     | EmbedFmt.expr ctx lctx infos =>
-      let subTt' := ExprWithCtx.tagExprInfos ctx lctx infos subTt
+      let subTt' := tagExprInfos ctx lctx infos subTt
       TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text subTt.stripTags)
     | EmbedFmt.goal ctx lctx g =>
       -- TODO(WN): use InteractiveGoal types here
@@ -110,39 +166,8 @@ partial def msgToInteractive (msgData : MessageData) (indent : Nat := 0) : IO (T
       TaggedText.tag (MsgEmbed.lazyTrace col cls ⟨msg⟩) (TaggedText.text subTt.stripTags)
     | EmbedFmt.ignoreTags => TaggedText.text subTt.stripTags
 
-structure MsgToInteractive where
-  msg : WithRpcRef MessageData
-  indent : Nat
-  deriving Inhabited, RpcEncoding
-
-builtin_initialize
-  registerRpcCallHandler `Lean.Widget.InteractiveDiagnostics.msgToInteractive MsgToInteractive (TaggedText MsgEmbed) fun ⟨⟨m⟩, i⟩ => RequestM.asTask do msgToInteractive m i
-
-structure InfoPopup where
-  type : Option CodeWithInfos
-  exprExplicit : Option CodeWithInfos
-  doc : Option String
-  deriving Inhabited, RpcEncoding
-
-builtin_initialize
-  registerRpcCallHandler `Lean.Widget.InteractiveDiagnostics.infoToInteractive (WithRpcRef InfoWithCtx) InfoPopup
-    fun ⟨i⟩ => RequestM.asTask do
-      i.ctx.runMetaM i.lctx do
-        let type? ← match (← i.info.type?) with
-          | some type => some <$> ExprWithCtx.tagged type
-          | none => none
-        let exprExplicit? ← match i.info with
-          | Elab.Info.ofTermInfo ti => some <$> ExprWithCtx.taggedExplicit ti.expr
-          | Elab.Info.ofFieldInfo fi => some (TaggedText.text fi.fieldName.toString)
-          | _ => none
-        return {
-          type := type?
-          exprExplicit := exprExplicit?
-          doc := ← i.info.docString? : InfoPopup
-        }
-
 /-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
-def msgToDiagnostic (text : FileMap) (m : Message) : ReaderT RpcSession IO Diagnostic := do
+def msgToInteractiveDiagnostic (text : FileMap) (m : Message) : IO InteractiveDiagnostic := do
   let low : Lsp.Position := text.leanPosToLspPos m.pos
   let fullHigh := text.leanPosToLspPos <| m.endPos.getD m.pos
   let high : Lsp.Position := match m.endPos with
@@ -162,27 +187,12 @@ def msgToDiagnostic (text : FileMap) (m : Message) : ReaderT RpcSession IO Diagn
     | MessageSeverity.warning     => DiagnosticSeverity.warning
     | MessageSeverity.error       => DiagnosticSeverity.error
   let source := "Lean 4"
-  let tt ← msgToInteractive m.data
-  let ttJson ← toJson <$> rpcEncode tt
   pure {
     range := range
     fullRange := fullRange
     severity? := severity
     source? := source
-    message := InteractiveMessage.pretty tt
-    taggedMsg? := ttJson
-  }
-
-def publishMessages (m : DocumentMeta) (msgLog : MessageLog) (hOut : IO.FS.Stream) (rpcSesh : RpcSession) : IO Unit := do
-  let diagnostics ← msgLog.msgs.mapM (msgToDiagnostic m.text · rpcSesh)
-  let diagParams : PublishDiagnosticsParams :=
-    { uri := m.uri
-      version? := some m.version
-      diagnostics := diagnostics.toArray
-    }
-  hOut.writeLspNotification {
-    method := "textDocument/publishDiagnostics"
-    param := toJson diagParams
+    message := ← msgToInteractive m.data
   }
 
 end Lean.Widget
diff --git a/src/Lean/Widget/InteractiveGoals.lean b/src/Lean/Widget/InteractiveGoal.lean
similarity index 59%
rename from src/Lean/Widget/InteractiveGoals.lean
rename to src/Lean/Widget/InteractiveGoal.lean
index 0b3bde869a..0a9da264ab 100644
--- a/src/Lean/Widget/InteractiveGoals.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -4,15 +4,33 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Wojciech Nawrocki
 -/
-import Lean.Widget.ExprWithCtx
+import Lean.Widget.InteractiveCode
 
-/-! RPC procedures for retrieving tactic and term goals with embedded `CodeWithInfos`s. -/
+/-! RPC procedures for retrieving tactic and term goals with embedded `CodeWithInfos`. -/
 -- TODO(WN): this module is mostly a slightly adapted copy of the corresponding `plainGoal/plainTemGoal` handlers
--- unify them somehow? or delete the plain ones.
+-- unify them
 
 namespace Lean.Widget
 open Server
 
+structure InteractiveGoal where
+  hyps      : Array (String × CodeWithInfos)
+  type      : CodeWithInfos
+  userName? : Option String
+  deriving Inhabited, RpcEncoding
+
+namespace InteractiveGoal
+
+def pretty (g : InteractiveGoal) : String :=
+  let ret := match g.userName? with
+    | some userName => s!"case {userName}\n"
+    | none          => ""
+  let hyps := g.hyps.map fun (name, tt) => s!"{name} : {tt.stripTags}"
+  let ret := ret ++ "\n".intercalate hyps.toList
+  ret ++ s!"⊢ {g.type.stripTags}"
+
+end InteractiveGoal
+
 structure InteractiveGoals where
   goals : Array InteractiveGoal
   deriving RpcEncoding
@@ -26,7 +44,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
     let lctx           := mvarDecl.lctx
     let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
     let mkExprWithCtx (e : Expr) : MetaM CodeWithInfos :=
-      ExprWithCtx.tagged e
+      exprToInteractive e
     withLCtx lctx mvarDecl.localInstances do
       let (hidden, hiddenProp) ← ToHide.collect mvarDecl.type
       -- The following two `let rec`s are being used to control the generated code size.
@@ -76,46 +94,4 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
         | name           => some <| toString name.eraseMacroScopes
       return { hyps := fmt, type := goalFmt, userName? }
 
-open RequestM in
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask InteractiveGoals) := do
-  let doc ← readDoc
-  let text := doc.meta.text
-  let hoverPos := text.lspPosToUtf8Pos p.position
-  -- NOTE: use `>=` since the cursor can be *after* the input
-  withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
-    (notFoundX := return { goals := #[] }) fun snap => do
-      for t in snap.cmdState.infoState.trees do
-        if let rs@(_ :: _) := t.goalsAt? doc.meta.text hoverPos then
-          let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
-            let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
-            let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
-            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (goalToInteractive g))
-          return { goals := goals.toArray }
-
-      return { goals := #[] }
-
-open RequestM in
-partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
-    : RequestM (RequestTask (Option InteractiveGoal)) := do
-  let doc ← readDoc
-  let text := doc.meta.text
-  let hoverPos := text.lspPosToUtf8Pos p.position
-  withWaitFindSnap doc (fun s => s.endPos > hoverPos)
-    (notFoundX := pure none) fun snap => do
-      for t in snap.cmdState.infoState.trees do
-        if let some (ci, i@(Elab.Info.ofTermInfo ti)) := t.termGoalAt? hoverPos then
-         let ty ← ci.runMetaM i.lctx do
-           Meta.instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
-         -- for binders, hide the last hypothesis (the binder itself)
-         let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
-         let goal ← ci.runMetaM lctx' do
-           Meta.withPPInaccessibleNames <| goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
-         --let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
-         return some goal
-      return none
-
-builtin_initialize
-  registerRpcCallHandler `Lean.Widget.getInteractiveGoals    Lsp.PlainGoalParams     InteractiveGoals         getInteractiveGoals
-  registerRpcCallHandler `Lean.Widget.getInteractiveTermGoal Lsp.PlainTermGoalParams (Option InteractiveGoal) getInteractiveTermGoal
-
 end Lean.Widget