chore: undo renaming

src/Lean/Elab/InfoTree/Main.lean

@@ -141,8 +141,8 @@ def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) :
   let output ← ctx.ppSyntax info.lctx info.output
   return f!"Macro expansion\n{stx}\n===>\n{output}"
 
-def PanelWidgetInfo.format (info : PanelWidgetInfo) : Format :=
-  f!"PanelWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
+def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
+  f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
   f!"FVarAlias {info.userName.eraseMacroScopes}"
@@ -158,7 +158,7 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofOptionInfo i         => i.format ctx
   | ofFieldInfo i          => i.format ctx
   | ofCompletionInfo i     => i.format ctx
-  | ofPanelWidgetInfo i    => pure <| i.format
+  | ofUserWidgetInfo i     => pure <| i.format
   | ofCustomInfo i         => pure <| Std.ToFormat.format i
   | ofFVarAliasInfo i      => pure <| i.format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
@@ -171,7 +171,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofOptionInfo _         => none
   | ofFieldInfo _          => none
   | ofCompletionInfo _     => none
-  | ofPanelWidgetInfo _    => none
+  | ofUserWidgetInfo _     => none
   | ofCustomInfo _         => none
   | ofFVarAliasInfo _      => none
   | ofFieldRedeclInfo _    => none

src/Lean/Elab/InfoTree/Types.lean

@@ -97,10 +97,11 @@ structure CustomInfo where
   stx : Syntax
   value : Dynamic
 
-/-- Information about a panel widget associated with a syntactic span.
+/-- Information about a user widget associated with a syntactic span.
+This must be a panel widget.
 A panel widget is a widget that can be displayed
 in the infoview alongside the goal state. -/
-structure PanelWidgetInfo extends Widget.WidgetInstance where
+structure UserWidgetInfo extends Widget.WidgetInstance where
   stx : Syntax
 
 /--
@@ -135,7 +136,7 @@ inductive Info where
   | ofOptionInfo (i : OptionInfo)
   | ofFieldInfo (i : FieldInfo)
   | ofCompletionInfo (i : CompletionInfo)
-  | ofPanelWidgetInfo (i : PanelWidgetInfo)
+  | ofUserWidgetInfo (i : UserWidgetInfo)
   | ofCustomInfo (i : CustomInfo)
   | ofFVarAliasInfo (i : FVarAliasInfo)
   | ofFieldRedeclInfo (i : FieldRedeclInfo)

src/Lean/Server/InfoUtils.lean

@@ -108,7 +108,7 @@ def Info.stx : Info → Syntax
   | ofFieldInfo i          => i.stx
   | ofCompletionInfo i     => i.stx
   | ofCustomInfo i         => i.stx
-  | ofPanelWidgetInfo i    => i.stx
+  | ofUserWidgetInfo i     => i.stx
   | ofFVarAliasInfo _      => .missing
   | ofFieldRedeclInfo i    => i.stx
 

src/Lean/Widget/UserWidget.lean

@@ -193,16 +193,16 @@ def savePanelWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m]
   let env ← getEnv
   let some (id, _) := moduleRegistry.getState env |>.find? hash
     | throwError s!"No widget module with hash {hash} registered"
-  pushInfoLeaf <| .ofPanelWidgetInfo { id, javascriptHash := hash, props, stx }
+  pushInfoLeaf <| .ofUserWidgetInfo { id, javascriptHash := hash, props, stx }
 
 /-! ## Retrieving panel widget instances -/
 
 #mkrpcenc WidgetInstance
 
-/-- Retrieve all the `PanelWidgetInfo`s at a particular position. -/
-def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List PanelWidgetInfo :=
+/-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/
+def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List UserWidgetInfo :=
   t.deepestNodes fun
-    | _ctx, i@(Info.ofPanelWidgetInfo wi), _cs => do
+    | _ctx, i@(Info.ofUserWidgetInfo wi), _cs => do
       if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
         -- Does the widget's line range contain `hoverLine`?
         guard <| (text.utf8PosToLspPos pos).line ≤ hoverLine ∧ hoverLine ≤ (text.utf8PosToLspPos tailPos).line
@@ -224,7 +224,7 @@ structure GetWidgetsResponse where
 #mkrpcenc GetWidgetsResponse
 
 open Lean Server RequestM in
-/-- Get the panel widgets present at a particular position. -/
+/-- Get the panel widgets present around a particular position. -/
 @[server_rpc_method]
 def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
   let doc ← readDoc
@@ -236,7 +236,7 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp
       | return ⟨∅⟩
     /- Panels from the infotree. -/
     let ws := widgetInfosAt? filemap snap.infoTree pos.line
-    let ws : Array PanelWidgetInstance := ws.toArray.map fun (wi : PanelWidgetInfo) =>
+    let ws : Array PanelWidgetInstance := ws.toArray.map fun (wi : UserWidgetInfo) =>
       { wi with
         range? := String.Range.toLspRange filemap <$> Syntax.getRange? wi.stx
         name? := toString wi.id }
@@ -258,23 +258,25 @@ syntax eraseWidgetSpec := "-" ident
 syntax showWidgetSpec := addWidgetSpec <|> eraseWidgetSpec
 /-- Use `show_panel_widgets [<widget>]` to mark that `<widget>`
 should always be displayed, including in downstream modules.
-Use `show_panel_widgets [<widget> with <props>] to have it
-displayed with the provided `<props>`.
 
 The type of `<widget>` must implement `Widget.ToModule`,
 and the type of `<props>` must implement `Server.RpcEncodable`.
 In particular, `<props> : Json` works.
 
+Use `show_panel_widgets [<widget> with <props>]`
+to specify the `<props>` that the widget should be given
+as arguments.
+
 Use `show_panel_widgets [local <widget> (with <props>)?]` to mark it
-for display in the current section, namespace, or file.
+for display in the current section, namespace, or file only.
 
 Use `show_panel_widgets [scoped <widget> (with <props>)?]` to mark it
-for display when the current namespace is open.
+for display only when the current namespace is open.
 
 Use `show_panel_widgets [-<widget>]` to temporarily hide a previously shown widget
 in the current section, namespace, or file.
-Note that global erasure is not possible, i.e.,
-`-<widget>` has no effect on downstream modules -/
+Note that persistent erasure is not possible, i.e.,
+`-<widget>` has no effect on downstream modules. -/
 syntax (name := showPanelWidgetsCmd) "show_panel_widgets " "[" sepBy1(showWidgetSpec, ", ") "]" : command
 
 def elabWidgetInstanceSpecAux (mod : Ident) (props : Term) : TermElabM Expr := do