diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index ac9f257f3e..b38e8a5369 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -17,6 +17,7 @@ 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
@@ -43,18 +44,24 @@ builtin_initialize
     (TaggedText MsgEmbed)
     fun ⟨⟨m⟩, i⟩ => RequestM.asTask do msgToInteractive m i (hasWidgets := true)
 
+/-- The information that the infoview uses to render a popup
+for when the user hovers over an expression.
+-/
 structure InfoPopup where
   type : Option CodeWithInfos
+  /-- Show the term with the implicit arguments. -/
   exprExplicit : Option CodeWithInfos
+  /-- Docstring. In markdown. -/
   doc : Option String
   deriving Inhabited, RpcEncoding
 
-builtin_initialize
-  registerBuiltinRpcProcedure
-    `Lean.Widget.InteractiveDiagnostics.infoToInteractive
-    (WithRpcRef InfoWithCtx)
-    InfoPopup
-    fun ⟨i⟩ => RequestM.asTask do
+/-- Given elaborator info for a particular subexpression. Produce the `InfoPopup`.
+
+The intended usage of this is for the infoview to pass the `InfoWithCtx` which
+was stored for a particular `SubexprInfo` tag in a `TaggedText` generated with `ppExprTagged`.
+ -/
+def makePopup : WithRpcRef InfoWithCtx → 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
@@ -74,6 +81,13 @@ builtin_initialize
           doc := ← i.info.docString? : InfoPopup
         }
 
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Lean.Widget.InteractiveDiagnostics.infoToInteractive
+    (WithRpcRef InfoWithCtx)
+    InfoPopup
+    makePopup
+
 builtin_initialize
   registerBuiltinRpcProcedure
     `Lean.Widget.getInteractiveGoals
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index 4fa6408b1c..dc93016dfa 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -6,12 +6,31 @@ 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`.
+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