diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index d88432929a..a50f534f32 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -127,51 +127,57 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) : O
       return i.contains hoverPos
     return false
 
+def Info.type? (i : Info) : MetaM (Option Expr) :=
+  match i with
+  | Info.ofTermInfo ti => Meta.inferType ti.expr
+  | Info.ofFieldInfo fi => Meta.inferType fi.val
+  | _ => return none
+
+def Info.docString? (i : Info) : MetaM (Option String) := do
+  if let Info.ofTermInfo ti := i then
+    if let some n := ti.expr.constName? then
+      return ← findDocString? n
+  if let Info.ofFieldInfo fi := i then
+    return ← findDocString? fi.projName
+  if let some ei := i.toElabInfo? then
+    return ← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind
+  return none
+
 /-- Construct a hover popup, if any, from an info node in a context.-/
-def Info.hoverMsg? (ci : ContextInfo) (i : Info) : IO (Option MessageData) := do
+def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
   ci.runMetaM i.lctx do
-    let mut msgs := #[]
+    let mut fmts := #[]
     try
-      if let some m ← termMsg? then
-        msgs := msgs.push m
+      if let some f ← fmtTerm? then
+        fmts := fmts.push f
     catch _ => pure ()
-    if let some m ← docMsg? then
-      msgs := msgs.push m
-    if msgs.isEmpty then
+    if let some m ← i.docString? then
+      fmts := fmts.push m
+    if fmts.isEmpty then
       none
     else
-      MessageData.withContext { env := ci.env, mctx := ci.mctx, lctx := i.lctx, opts := ci.options }
-        <| MessageData.withNamingContext { currNamespace := ci.currNamespace, openDecls := ci.openDecls }
-        <| m!"\n***\n".joinSep msgs.toList
+      f!"\n***\n".joinSep fmts.toList
+
 where
-  termMsg? : MetaM (Option MessageData) := do
+  fmtTerm? : MetaM (Option Format) := do
     match i with
     | Info.ofTermInfo ti =>
       let tp ← Meta.inferType ti.expr
-      -- try not to show too scary internals
-      -- TODO(WN): this check is now quite costly; should we do it in `MessageData.format`?
       let eFmt ← Meta.ppExpr ti.expr
-      let msg := if isAtomicFormat eFmt then m!"{ti.expr} : {tp}" else m!"{tp}"
-      return m!"```lean
-{msg}
+      let tpFmt ← Meta.ppExpr tp
+      -- try not to show too scary internals
+      let fmt := if isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else f!"{tpFmt}"
+      return some f!"```lean
+{fmt}
 ```"
     | Info.ofFieldInfo fi =>
       let tp ← Meta.inferType fi.val
-      return m!"```lean
-{fi.fieldName} : {tp}
+      let tpFmt ← Meta.ppExpr tp
+      return some f!"```lean
+{fi.fieldName} : {tpFmt}
 ```"
     | _ => return none
 
-  docMsg? : MetaM (Option MessageData) := do
-    if let Info.ofTermInfo ti := i then
-      if let some n := ti.expr.constName? then
-        return (← findDocString? n).map toMessageData
-    if let Info.ofFieldInfo fi := i then
-      return (← findDocString? fi.projName).map toMessageData
-    if let some ei := i.toElabInfo? then
-      return (← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind).map toMessageData
-    return none
-
   isAtomicFormat : Format → Bool
     | Std.Format.text _    => true
     | Std.Format.group f _ => isAtomicFormat f
@@ -179,11 +185,6 @@ where
     | Std.Format.tag _ f   => isAtomicFormat f
     | _                    => false
 
-def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
-  match ← i.hoverMsg? ci with
-  | none => return none
-  | some m => m.format
-
 structure GoalsAtResult where
   ctxInfo    : ContextInfo
   tacticInfo : TacticInfo
diff --git a/src/Lean/Widget/InteractiveDiagnostics.lean b/src/Lean/Widget/InteractiveDiagnostics.lean
index 909948c167..cdd87e951c 100644
--- a/src/Lean/Widget/InteractiveDiagnostics.lean
+++ b/src/Lean/Widget/InteractiveDiagnostics.lean
@@ -63,7 +63,8 @@ where
       fileMap := arbitrary
       options := ctx.opts
       currNamespace := nCtx.currNamespace
-      openDecls := nCtx.openDecls }
+      openDecls := nCtx.openDecls
+    }
     let (fmt, infos) ← ci.runMetaM ctx.lctx (ExprWithCtx.formatInfos e)
     let t ← pushEmbed <| EmbedFmt.expr ci ctx.lctx infos
     return Format.tag t fmt
@@ -71,38 +72,75 @@ where
   | nCtx, some ctx,  ofGoal mvarId            => withIgnoreTags <| ppGoal (mkPPContext nCtx ctx) mvarId
   | nCtx, _,         withContext ctx d        => go nCtx ctx d
   | _,    ctx,       withNamingContext nCtx d => go nCtx ctx d
-  | nCtx, ctx,       tagged n d               => do
+  | nCtx, ctx,       tagged t d               => do
     -- tagged is *almost* perfect for detecting traces
     -- expect for the following two other occurrences:
     -- src/Lean/Elab/Term.lean:454
     -- src/Lean/Elab/Tactic/Basic.lean:33
-    let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx n d
-    Format.tag f <$> go nCtx ctx d
+    if let Name.str cls "_traceCtx" _ := t then
+      let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx cls d
+      Format.tag f s!"[{cls}] (trace hidden)"
+    else
+      go nCtx ctx d
   | nCtx, ctx,       nest n d                 => Format.nest n <$> go nCtx ctx d
   | nCtx, ctx,       compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
   | nCtx, ctx,       group d                  => Format.group <$> go nCtx ctx d
   | nCtx, ctx,       node ds                  => Format.nest 2 <$> ds.foldlM (fun r d => do let d ← go nCtx ctx d; pure $ r ++ Format.line ++ d) Format.nil
 
-private partial def msgToInteractive (msgData : MessageData) : IO (TaggedText MsgEmbed) := do
+partial def msgToInteractive (msgData : MessageData) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do
   let (fmt, embeds) ← msgToInteractiveAux msgData
-  let tt := TaggedText.prettyTagged fmt
+  let tt := TaggedText.prettyTagged fmt indent
   /- Here we rewrite a `TaggedText Nat` corresponding to a whole `MessageData` into one where
   the tags are `TaggedText MsgEmbed`s corresponding to embedded objects with their subtree
   empty (`text ""`). In other words, we terminate the `MsgEmbed`-tagged -tree at embedded objects
   and store the pretty-printed embed (which can itself be a `TaggedText`) in the tag. -/
-  tt.rewriteM fun n subTt =>
+  tt.rewriteM fun (n, col) subTt =>
     match embeds.get! n with
     | EmbedFmt.expr ctx lctx infos =>
       let subTt' := ExprWithCtx.tagExprInfos ctx lctx infos subTt
-      TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text "")
+      TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text subTt.stripTags)
     | EmbedFmt.goal ctx lctx g =>
       -- TODO(WN): use InteractiveGoal types here
       unreachable!
-    | EmbedFmt.lazyTrace nCtx ctx? n m =>
-      -- TODO(WN): TraceExplorer component
-      TaggedText.tag (MsgEmbed.lazyTrace ⟨"1337"⟩) (TaggedText.text "")
+    | EmbedFmt.lazyTrace nCtx ctx? cls m =>
+      let msg :=
+        match ctx? with
+        | some ctx => MessageData.withNamingContext nCtx <| MessageData.withContext ctx m
+        | none     => MessageData.withNamingContext nCtx m
+      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
   let low : Lsp.Position := text.leanPosToLspPos m.pos
@@ -140,7 +178,8 @@ def publishMessages (m : DocumentMeta) (msgLog : MessageLog) (hOut : IO.FS.Strea
   let diagParams : PublishDiagnosticsParams :=
     { uri := m.uri
       version? := some m.version
-      diagnostics := diagnostics.toArray }
+      diagnostics := diagnostics.toArray
+    }
   hOut.writeLspNotification {
     method := "textDocument/publishDiagnostics"
     param := toJson diagParams