chore: revert "refactor: replace InfoWithCtx with ExprWithCtx"

This reverts commit db342793d53c986b8794084196552c33711f9091.

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -57,33 +57,34 @@ 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 `ExprWithCtx` which
+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 ExprWithCtx → RequestM (RequestTask InfoPopup)
+def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
     | ⟨i⟩ => RequestM.asTask do
-      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
+      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
         return {
           type := type?
-          exprExplicit := some tt
-          doc := doc? : InfoPopup
+          exprExplicit := exprExplicit?
+          doc := ← i.info.docString? : InfoPopup
         }
 
 builtin_initialize
   registerBuiltinRpcProcedure
     `Lean.Widget.InteractiveDiagnostics.infoToInteractive
-    (WithRpcRef ExprWithCtx)
+    (WithRpcRef InfoWithCtx)
     InfoPopup
     makePopup
 
@@ -131,25 +132,23 @@ builtin_initialize
 
 structure GetGoToLocationParams where
   kind : GoToKind
-  info : WithRpcRef ExprWithCtx
+  info : WithRpcRef InfoWithCtx
   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)
-    getGoToLocation
+    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
 
 end Lean.Widget

src/Lean/Widget/Basic.lean

@@ -6,23 +6,37 @@ namespace Lean.Widget
 
 open Elab Server
 
-/-- Expression with the context required to render it interactively in the infoview. -/
+/-- 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 }
-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
-  }
+/-- 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
 
 instance : ToJson FVarId := ⟨fun f => toJson f.name⟩
 instance : ToJson MVarId := ⟨fun f => toJson f.name⟩

src/Lean/Widget/InteractiveCode.lean

@@ -17,8 +17,8 @@ open Server
 
 /-- Information about a subexpression within delaborated code. -/
 structure SubexprInfo where
-  /-- The Expression and context node with the semantics of this part of the output. -/
-  info : WithRpcRef ExprWithCtx
+  /-- The `Elab.Info` node with the semantics of this part of the output. -/
+  info : WithRpcRef InfoWithCtx
   /-- The position of this subexpression within the top-level expression.
   See `Lean.SubExpr`. -/
   subexprPos : Lean.SubExpr.Pos
@@ -40,9 +40,8 @@ where
   go (tt : TaggedText (Nat × Nat)) :=
     tt.rewrite fun (n, _) subTt =>
       match infos.find? n with
-      | 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
+      | none   => go subTt
+      | some i => TaggedText.tag ⟨WithRpcRef.mk { ctx, info := i }, n⟩ (go subTt)
 
 def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
   let optsPerPos := if explicit then