feat: bundle of widget improvements (#2964)

Implements RFC #2963.

Leftover tasks:
- [x] Provide companion PR to vscode-lean4 (leanprover/vscode-lean4#376)
- [x] Companion PR to std4 (leanprover/std4#467)
- [x] Companion PR to ProofWidgets4
(leanprover-community/ProofWidgets4#36)
- [X] Companion commit to mathlib4
(0f4660f655)
- [ ] ~~Update the manual chapter~~ (will do in a follow-up)

doc/examples/widgets.lean

@@ -15,9 +15,8 @@ sections of a Lean document. User widgets are rendered in the Lean infoview.
 To try it out, simply type in the following code and place your cursor over the `#widget` command.
 -/
 
-@[widget]
-def helloWidget : UserWidgetDefinition where
-  name := "Hello"
+@[widget_module]
+def helloWidget : Widget.Module where
   javascript := "
     import * as React from 'react';
     export default function(props) {
@@ -25,7 +24,7 @@ def helloWidget : UserWidgetDefinition where
       return React.createElement('p', {}, name + '!')
     }"
 
-#widget helloWidget .null
+#widget helloWidget
 
 /-!
 If you want to dive into a full sample right away, check out
@@ -56,7 +55,11 @@ to the React component. In our first invocation of `#widget`, we set it to `.nul
 happens when you type in:
 -/
 
-#widget helloWidget (Json.mkObj [("name", "<your name here>")])
+structure HelloWidgetProps where
+  name? : Option String := none
+  deriving Server.RpcEncodable
+
+#widget helloWidget with { name? := "<your name here>" : HelloWidgetProps }
 
 /-!
 💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
@@ -132,9 +135,8 @@ on this we either display an `InteractiveCode` with the type, `mapRpcError` the
 to turn it into a readable message, or show a `Loading..` message, respectively.
 -/
 
-@[widget]
-def checkWidget : UserWidgetDefinition where
-  name := "#check as a service"
+@[widget_module]
+def checkWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
@@ -160,7 +162,7 @@ export default function(props) {
 Finally we can try out the widget.
 -/
 
-#widget checkWidget .null
+#widget checkWidget
 
 /-!
 ![`#check` as a service](../images/widgets_caas.png)
@@ -193,9 +195,8 @@ interact with the text editor.
 You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52)
 -/
 
-@[widget]
-def insertTextWidget : UserWidgetDefinition where
-  name := "textInserter"
+@[widget_module]
+def insertTextWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
@@ -213,4 +214,4 @@ export default function(props) {
 
 /-! Finally, we can try this out: -/
 
-#widget insertTextWidget .null
+#widget insertTextWidget

src/Lean/Attributes.lean

@@ -330,7 +330,7 @@ private def AttributeExtension.mkInitial : IO AttributeExtensionState := do
 
 unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl :=
   match env.find? declName with
-  | none      => throw ("unknow constant '" ++ toString declName ++ "'")
+  | none      => throw ("unknown constant '" ++ toString declName ++ "'")
   | some info =>
     match info.type with
     | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName

src/Lean/Elab/InfoTree/Main.lean

@@ -142,7 +142,7 @@ def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) :
   return f!"Macro expansion\n{stx}\n===>\n{output}"
 
 def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
-  f!"UserWidget {info.widgetId}\n{Std.ToFormat.format info.props}"
+  f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
   f!"FVarAlias {info.userName.eraseMacroScopes}"

src/Lean/Elab/InfoTree/Types.lean

@@ -9,6 +9,8 @@ import Lean.Data.OpenDecl
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Data.Json
+import Lean.Server.Rpc.Basic
+import Lean.Widget.Types
 
 namespace Lean.Elab
 
@@ -95,17 +97,12 @@ structure CustomInfo where
   stx : Syntax
   value : Dynamic
 
-/-- An info that represents a user-widget.
-User-widgets are custom pieces of code that run on the editor client.
-You can learn about user widgets at `src/Lean/Widget/UserWidget`
--/
-structure UserWidgetInfo where
+/-- 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 UserWidgetInfo extends Widget.WidgetInstance where
   stx : Syntax
-  /-- Id of `WidgetSource` object to use. -/
-  widgetId : Name
-  /-- Json representing the props to be loaded in to the component. -/
-  props : Json
-  deriving Inhabited
 
 /--
 Specifies that the given free variables should be considered semantically identical.

src/Lean/Server/Rpc/Basic.lean

@@ -62,18 +62,28 @@ def rpcReleaseRef (r : Lsp.RpcRef) : StateM RpcObjectStore Bool := do
   else
     return false
 
-/--
-`RpcEncodable α` means that `α` can be serialized in the RPC system of the Lean server.
-This is required when `α` contains fields which should be serialized as an RPC reference
-instead of being sent in full.
-The type wrapper `WithRpcRef` is used for these fields which should be sent as
-a reference.
+/-- `RpcEncodable α` means that `α` can be deserialized from and serialized into JSON
+for the purpose of receiving arguments to and sending return values from
+Remote Procedure Calls (RPCs).
 
-- Any type with `FromJson` and `ToJson` instance is automatically `RpcEncodable`.
-- If a type has an `Dynamic` instance, then `WithRpcRef` can be used for its references.
-- `deriving RpcEncodable` acts like `FromJson`/`ToJson` but marshalls any `WithRpcRef` fields
-  as `Lsp.RpcRef`s.
--/
+Any type with `FromJson` and `ToJson` instances is `RpcEncodable`.
+
+Furthermore, types that do not have these instances may still be `RpcEncodable`.
+Use `deriving RpcEncodable` to automatically derive instances for such types.
+
+This occurs when `α` contains data that should not or cannot be serialized:
+for instance, heavy objects such as `Lean.Environment`, or closures.
+For such data, we use the `WithRpcRef` marker.
+Note that for `WithRpcRef α` to be `RpcEncodable`,
+`α` must have a `TypeName` instance
+
+On the server side, `WithRpcRef α` is just a structure
+containing a value of type `α`.
+On the client side, it is an opaque reference of (structural) type `Lsp.RpcRef`.
+Thus, `WithRpcRef α` is cheap to transmit over the network
+but may only be accessed on the server side.
+In practice, it is used by the client to pass data
+between various RPC methods provided by the server. -/
 -- TODO(WN): for Lean.js, compile `WithRpcRef` to "opaque reference" on the client
 class RpcEncodable (α : Type) where
   rpcEncode : α → StateM RpcObjectStore Json
@@ -103,7 +113,15 @@ instance [RpcEncodable α] [RpcEncodable β] : RpcEncodable (α × β) where
     let (a, b) ← fromJson? j
     return (← rpcDecode a, ← rpcDecode b)
 
-/-- Marks fields to encode as opaque references in LSP packets. -/
+instance [RpcEncodable α] : RpcEncodable (StateM RpcObjectStore α) where
+  rpcEncode fn := fn >>= rpcEncode
+  rpcDecode j := do
+    let a : α ← rpcDecode j
+    return return a
+
+/-- Marks values to be encoded as opaque references in RPC packets.
+
+See the docstring for `RpcEncodable`. -/
 structure WithRpcRef (α : Type u) where
   val : α
   deriving Inhabited

src/Lean/Server/Rpc/Deriving.lean

@@ -42,7 +42,10 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
 
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
 
-  `(structure RpcEncodablePacket where
+  let indName := mkIdent indVal.name
+  `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
+    structure RpcEncodablePacket where
       $[($fieldIds : $fieldTys)]*
       deriving FromJson, ToJson
 
@@ -55,6 +58,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       dec j := do
         let a : RpcEncodablePacket ← fromJson? j
         return { $[$decInits],* }
+    end $indName
   )
 
 private def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
@@ -92,7 +96,10 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
   let typeId ← `(@$(mkIdent indVal.name) $paramIds*)
 
-  `(inductive RpcEncodablePacket where
+  let indName := mkIdent indVal.name
+  `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
+    inductive RpcEncodablePacket where
       $[$ctors:ctor]*
       deriving FromJson, ToJson
 
@@ -107,6 +114,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
         have inst : RpcEncodable $typeId := { rpcEncode := enc, rpcDecode := dec }
         let pkt : RpcEncodablePacket ← fromJson? j
         id <| match pkt with $[$decodes:matchAlt]*
+    end $indName
   )
 
 /-- Creates an `RpcEncodablePacket` for `typeName`. For structures, the packet is a structure

src/Lean/Widget/Basic.lean

@@ -2,6 +2,7 @@ import Lean.Elab.InfoTree
 import Lean.Message
 import Lean.Server.Rpc.Basic
 import Lean.Server.InfoUtils
+import Lean.Widget.Types
 
 namespace Lean.Widget
 

src/Lean/Widget/Types.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2023 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
+import Lean.Server.Rpc.Basic
+
+namespace Lean.Widget
+
+/-- An instance of a widget component:
+the identifier of a widget module and the hash of its JS source code
+together with props.
+
+See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
+for more information about widgets. -/
+structure WidgetInstance where
+  /-- Name of the `@[widget_module]`. -/
+  id : Name
+  /-- Hash of the JS source of the widget module. -/
+  javascriptHash : UInt64
+  /-- Arguments to be passed to the component's default exported function.
+
+  Props may contain RPC references,
+  so must be stored as a computation
+  with access to the RPC object store. -/
+  props : StateM Server.RpcObjectStore Json
+
+end Lean.Widget

src/Lean/Widget/UserWidget.lean

@@ -2,29 +2,309 @@
 Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Authors: E.W.Ayers
+Authors: E.W.Ayers, Wojciech Nawrocki
 -/
 import Lean.Elab.Eval
 import Lean.Server.Rpc.RequestHandling
 
-open Lean
+namespace Lean.Server
+open Elab Command in
+/-- Derive `Lean.Server.RpcEncodable` for a type.
+
+TODO: remove after update-stage0 -/
+elab "#mkrpcenc" n:ident : command => do
+  elabCommand <| ← `(
+    namespace $n
+    deriving instance Lean.Server.RpcEncodable for $n
+    end $n
+  )
+end Lean.Server
 
 namespace Lean.Widget
+open Meta Elab
 
-/-- A custom piece of code that is run on the editor client.
+/-- A widget module is a unit of source code that can execute in the infoview.
 
-The editor can use the `Lean.Widget.getWidgetSource` RPC method to
-get this object.
+Every module definition must either be annotated with `@[widget_module]`,
+or use a value of `javascript` identical to that of another definition
+annotated with `@[widget_module]`.
+This makes it possible for the infoview to load the module.
 
-See the [manual entry](doc/widgets.md) above this declaration for more information on
-how to use the widgets system.
+See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
+for more information on how to use the widgets system. -/
+structure Module where
+  /-- A JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
+  intended for use in user widgets.
+
+  The JS environment in which modules execute
+  provides a fixed set of libraries accessible via direct `import`,
+  notably [`@leanprover/infoview`](https://www.npmjs.com/package/@leanprover/infoview)
+  and [`react`](https://www.npmjs.com/package/react).
+
+  To initialize this field from an external JS file,
+  you may use `include_str "path"/"to"/"file.js"`.
+  However **beware** that this does not register a dependency with Lake,
+  so your Lean module will not automatically be rebuilt
+  when the `.js` file changes. -/
+  javascript : String
+  /-- The hash is cached to avoid recomputing it whenever the `Module` is used. -/
+  javascriptHash : { x : UInt64 // x = hash javascript } := ⟨hash javascript, rfl⟩
+
+private unsafe def evalModuleUnsafe (e : Expr) : MetaM Module :=
+  evalExpr' Module ``Module e
+
+@[implemented_by evalModuleUnsafe]
+opaque evalModule (e : Expr) : MetaM Module
+
+private unsafe def evalWidgetInstanceUnsafe (e : Expr) : MetaM WidgetInstance :=
+  evalExpr' WidgetInstance ``WidgetInstance e
+
+@[implemented_by evalWidgetInstanceUnsafe]
+opaque evalWidgetInstance (e : Expr) : MetaM WidgetInstance
+
+/-! ## Storage of widget modules -/
+
+class ToModule (α : Type u) where
+  toModule : α → Module
+
+instance : ToModule Module := ⟨id⟩
+
+/-- Every constant `c : α` marked with `@[widget_module]` is registered here.
+The registry maps `hash (toModule c).javascript` to ``(`c, `(@toModule α inst c))``
+where `inst : ToModule α` is synthesized during registration time
+and stored thereafter. -/
+private abbrev ModuleRegistry := SimplePersistentEnvExtension
+  (UInt64 × Name × Expr)
+  (RBMap UInt64 (Name × Expr) compare)
+
+builtin_initialize moduleRegistry : ModuleRegistry ←
+  registerSimplePersistentEnvExtension {
+    addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
+    addEntryFn    := fun s n => s.insert n.1 n.2
+    toArrayFn     := fun es => es.toArray
+  }
+
+private def widgetModuleAttrImpl : AttributeImpl where
+  name := `widget_module
+  descr := "Registers a widget module. Its type must implement Lean.Widget.ToModule."
+  applicationTime := AttributeApplicationTime.afterCompilation
+  add decl _stx _kind := Prod.fst <$> MetaM.run do
+    let e ← mkAppM ``ToModule.toModule #[.const decl []]
+    let mod ← evalModule e
+    let env ← getEnv
+    if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then
+      logWarning m!"A widget module with the same hash(JS source code) was already registered at {Expr.const n []}."
+    setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
+
+builtin_initialize registerBuiltinAttribute widgetModuleAttrImpl
+
+/-! ## Retrieval of widget modules -/
+
+structure GetWidgetSourceParams where
+  /-- Hash of the JS module to retrieve. -/
+  hash : UInt64
+  pos : Lean.Lsp.Position
+  deriving ToJson, FromJson
 
--/
 structure WidgetSource where
-  /-- Sourcetext of the code to run.-/
+  /-- Sourcetext of the JS module to run. -/
   sourcetext : String
   deriving Inhabited, ToJson, FromJson
 
+open Server RequestM in
+@[server_rpc_method]
+def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
+  let doc ← readDoc
+  let pos := doc.meta.text.lspPosToUtf8Pos args.pos
+  let notFound := throwThe RequestError ⟨.invalidParams, s!"No widget module with hash {args.hash} registered"⟩
+  withWaitFindSnap doc (notFoundX := notFound)
+    (fun s => s.endPos >= pos || (moduleRegistry.getState s.env).contains args.hash)
+    fun snap => do
+      if let some (_, e) := moduleRegistry.getState snap.env |>.find? args.hash then
+        runTermElabM snap do
+          return { sourcetext := (← evalModule e).javascript }
+      else
+        notFound
+
+/-! ## Storage of panel widget instances -/
+
+inductive PanelWidgetsExtEntry where
+  | «global» (n : Name)
+  | «local» (wi : WidgetInstance)
+
+/-- Keeps track of panel widget instances that should be displayed.
+
+Instances can be registered for display global
+(i.e., persisted in `.olean`s) and locally (not persisted)
+
+For globally displayed widgets
+we cannot store a `WidgetInstance` in the persistent state
+because it contains a `StateM` closure.
+Instead, we add a global constant of type `WidgetInstance`
+to the environment, and store its name in the extension.
+
+For locally displayed ones, we just store a `WidgetInstance`
+in the extension directly.
+This is okay because it is never persisted.
+
+The (persistent) entries are then of the form `(h, n)`
+where `h` is a hash stored in the `moduleRegistry`
+and `n` is the name of a `WidgetInstance` global constant.
+
+The extension state maps each `h` as above
+to a list of entries that can be either global or local ones.
+Each element of the state indicates that the widget module `h`
+should be displayed with the given `WidgetInstance` as its arguments.
+
+This is similar to a parametric attribute, except that:
+- parametric attributes map at most one parameter to one tagged declaration,
+  whereas we may display multiple instances of a single widget module; and
+- parametric attributes use the same type for local and global entries,
+  which we cannot do owing to the closure. -/
+private abbrev PanelWidgetsExt := SimpleScopedEnvExtension
+  (UInt64 × Name)
+  (RBMap UInt64 (List PanelWidgetsExtEntry) compare)
+
+builtin_initialize panelWidgetsExt : PanelWidgetsExt ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun s (h, n) => s.insert h (.global n :: s.findD h [])
+    initial  := .empty
+  }
+
+def evalPanelWidgets : MetaM (Array WidgetInstance) := do
+  let mut ret := #[]
+  for (_, l) in panelWidgetsExt.getState (← getEnv) do
+    for e in l do
+      match e with
+      | .global n =>
+        let wi ← evalWidgetInstance (mkConst n)
+        ret := ret.push wi
+      | .local wi => ret := ret.push wi
+  return ret
+
+def addPanelWidgetGlobal [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit := do
+  panelWidgetsExt.add (h, n)
+
+def addPanelWidgetScoped [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit := do
+  panelWidgetsExt.add (h, n) .scoped
+
+def addPanelWidgetLocal [Monad m] [MonadEnv m] (wi : WidgetInstance) : m Unit := do
+  modifyEnv fun env => panelWidgetsExt.modifyState env fun s =>
+    s.insert wi.javascriptHash (.local wi :: s.findD wi.javascriptHash [])
+
+def erasePanelWidget [Monad m] [MonadEnv m] (h : UInt64) : m Unit := do
+  modifyEnv fun env => panelWidgetsExt.modifyState env fun st => st.erase h
+
+/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
+`hash` must be `hash (toModule c).javascript`
+where `c` is some global constant annotated with `@[widget_module]`. -/
+def savePanelWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m]
+    (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) : m Unit := do
+  let env ← getEnv
+  let some (id, _) := moduleRegistry.getState env |>.find? hash
+    | throwError s!"No widget module with hash {hash} registered"
+  pushInfoLeaf <| .ofUserWidgetInfo { id, javascriptHash := hash, props, stx }
+
+/-! ## `show_panel_widgets` command -/
+
+syntax widgetInstanceSpec := ident ("with " term)?
+
+def elabWidgetInstanceSpecAux (mod : Ident) (props : Term) : TermElabM Expr := do
+  Term.elabTerm (expectedType? := mkConst ``WidgetInstance) <| ← `(
+    { id := $(quote mod.getId)
+      javascriptHash := (ToModule.toModule $mod).javascriptHash
+      props := Server.RpcEncodable.rpcEncode $props })
+
+def elabWidgetInstanceSpec : TSyntax ``widgetInstanceSpec → TermElabM Expr
+  | `(widgetInstanceSpec| $mod:ident) => do
+    elabWidgetInstanceSpecAux mod (← ``(Json.mkObj []))
+  | `(widgetInstanceSpec| $mod:ident with $props:term) => do
+    elabWidgetInstanceSpecAux mod props
+  | _ => throwUnsupportedSyntax
+
+syntax addWidgetSpec := Parser.Term.attrKind widgetInstanceSpec
+syntax eraseWidgetSpec := "-" ident
+syntax showWidgetSpec := addWidgetSpec <|> eraseWidgetSpec
+/-- Use `show_panel_widgets [<widget>]` to mark that `<widget>`
+should always be displayed, including in downstream modules.
+
+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 only.
+
+Use `show_panel_widgets [scoped <widget> (with <props>)?]` to mark it
+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 persistent erasure is not possible, i.e.,
+`-<widget>` has no effect on downstream modules. -/
+syntax (name := showPanelWidgetsCmd) "show_panel_widgets " "[" sepBy1(showWidgetSpec, ", ") "]" : command
+
+open Command in
+@[command_elab showPanelWidgetsCmd] def elabShowPanelWidgetsCmd : CommandElab
+  | `(show_panel_widgets [ $ws ,*]) => liftTermElabM do
+    for w in ws.getElems do
+      match w with
+      | `(showWidgetSpec| - $mod:ident) =>
+        let mod : Term ← ``(ToModule.toModule $mod)
+        let mod : Expr ← Term.elabTerm (expectedType? := mkConst ``Module) mod
+        let mod : Module ← evalModule mod
+        erasePanelWidget mod.javascriptHash
+      | `(showWidgetSpec| $attr:attrKind $spec:widgetInstanceSpec) =>
+        let attr ← liftMacroM <| toAttributeKind attr
+        let wiExpr ← elabWidgetInstanceSpec spec
+        let wi ← evalWidgetInstance wiExpr
+        if let .local := attr then
+          addPanelWidgetLocal wi
+        else
+          let name ← mkFreshUserName (wi.id ++ `_instance)
+          let wiExpr ← instantiateMVars wiExpr
+          if wiExpr.hasMVar then
+            throwError "failed to compile expression, it contains metavariables{indentExpr wiExpr}"
+          addAndCompile <| Declaration.defnDecl {
+            name
+            levelParams := []
+            type := mkConst ``WidgetInstance
+            value := wiExpr
+            hints := .opaque
+            safety := .safe
+          }
+          if let .global := attr then
+            addPanelWidgetGlobal wi.javascriptHash name
+          else
+            addPanelWidgetScoped wi.javascriptHash name
+      | _ => throwUnsupportedSyntax
+  | _ => throwUnsupportedSyntax
+
+/-! ## `#widget` command -/
+
+/-- Use `#widget <widget>` to display a panel widget,
+and `#widget <widget> with <props>` to display it with the given props.
+Useful for debugging widgets.
+
+The type of `<widget>` must implement `Widget.ToModule`,
+and the type of `<props>` must implement `Server.RpcEncodable`.
+In particular, `<props> : Json` works. -/
+syntax (name := widgetCmd) "#widget " widgetInstanceSpec : command
+
+open Command in
+@[command_elab widgetCmd] def elabWidgetCmd : CommandElab
+  | stx@`(#widget $s) => liftTermElabM do
+    let wi : Expr ← elabWidgetInstanceSpec s
+    let wi : WidgetInstance ← evalWidgetInstance wi
+    savePanelWidgetInfo wi.javascriptHash wi.props stx
+  | _ => throwUnsupportedSyntax
+
+/-! ## Deprecated definitions -/
+
 /-- Use this structure and the `@[widget]` attribute to define your own widgets.
 
 ```lean
@@ -42,149 +322,101 @@ structure UserWidgetDefinition where
   javascript: String
   deriving Inhabited, ToJson, FromJson
 
-structure UserWidget where
-  id : Name
-  /-- Pretty name of widget to display to the user.-/
-  name : String
-  javascriptHash: UInt64
-  deriving Inhabited, ToJson, FromJson
+instance : ToModule UserWidgetDefinition where
+  toModule uwd := { uwd with }
 
-private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension
-    (UInt64 × Name)
-    (RBMap UInt64 Name compare)
-
--- Mapping widgetSourceId to hash of sourcetext
-builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension
-builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ←
-  registerSimplePersistentEnvExtension {
-    addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
-    addEntryFn    := fun s n => s.insert n.1 n.2
-    toArrayFn     := fun es => es.toArray
-  }
-
-private unsafe def getUserWidgetDefinitionUnsafe
-  (decl : Name) : CoreM UserWidgetDefinition :=
-  evalConstCheck UserWidgetDefinition ``UserWidgetDefinition decl
-
-@[implemented_by getUserWidgetDefinitionUnsafe]
-private opaque getUserWidgetDefinition
-  (decl : Name) : CoreM UserWidgetDefinition
-
-private def attributeImpl : AttributeImpl where
+private def widgetAttrImpl : AttributeImpl where
   name := `widget
-  descr := "Mark a string as static code that can be loaded by a widget handler."
+  descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead."
   applicationTime := AttributeApplicationTime.afterCompilation
-  add decl _stx _kind := do
-    let env ← getEnv
-    let defn ← getUserWidgetDefinition decl
-    let javascriptHash := hash defn.javascript
-    let env := userWidgetRegistry.insert env decl {id := decl, name := defn.name, javascriptHash}
-    let env := widgetSourceRegistry.addEntry env (javascriptHash, decl)
-    setEnv <| env
+  add := widgetModuleAttrImpl.add
 
-builtin_initialize registerBuiltinAttribute attributeImpl
+builtin_initialize registerBuiltinAttribute widgetAttrImpl
 
-/-- Input for `getWidgetSource` RPC. -/
-structure GetWidgetSourceParams where
-  /-- The hash of the sourcetext to retrieve. -/
-  hash: UInt64
-  pos : Lean.Lsp.Position
-  deriving ToJson, FromJson
+private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
+    (id : Name) : m UserWidgetDefinition := do
+  ofExcept <| (← getEnv).evalConstCheck UserWidgetDefinition (← getOptions) ``UserWidgetDefinition id
 
-open Server RequestM in
-@[server_rpc_method]
-def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
-  let doc ← readDoc
-  let pos := doc.meta.text.lspPosToUtf8Pos args.pos
-  let notFound := throwThe RequestError ⟨.invalidParams, s!"No registered user-widget with hash {args.hash}"⟩
-  withWaitFindSnap doc (notFoundX := notFound)
-    (fun s => s.endPos >= pos || (widgetSourceRegistry.getState s.env).contains args.hash)
-    fun snap => do
-      if let some id := widgetSourceRegistry.getState snap.env |>.find? args.hash then
-        runCoreM snap do
-          return {sourcetext := (← getUserWidgetDefinition id).javascript}
-      else
-        notFound
+@[implemented_by evalUserWidgetDefinitionUnsafe]
+opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
+    (id : Name) : m UserWidgetDefinition
 
-open Lean Elab
+/-- Save a user-widget instance to the infotree.
+    The given `widgetId` should be the declaration name of the widget definition. -/
+@[deprecated savePanelWidgetInfo] def saveWidgetInfo
+    [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadInfoTree m]
+    (widgetId : Name) (props : Json) (stx : Syntax) : m Unit := do
+  let uwd ← evalUserWidgetDefinition widgetId
+  savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx
 
-/--
-  Try to retrieve the `UserWidgetInfo` at a particular position.
--/
-def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List UserWidgetInfo :=
+/-! ## Retrieving panel widget instances -/
+
+#mkrpcenc WidgetInstance
+
+/-- 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.ofUserWidgetInfo wi), _cs => do
       if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
-        let trailSize := i.stx.getTrailingSize
-        -- show info at EOF even if strictly outside token + trail
-        let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
-        guard <| pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + trailSize || atEOF)
+        -- Does the widget's line range contain `hoverLine`?
+        guard <| (text.utf8PosToLspPos pos).line ≤ hoverLine ∧ hoverLine ≤ (text.utf8PosToLspPos tailPos).line
         return wi
       else
         failure
     | _, _, _ => none
 
-/-- UserWidget accompanied by component props. -/
-structure UserWidgetInstance extends UserWidget where
-  /-- Arguments to be fed to the widget's main component. -/
-  props : Json
-  /-- The location of the widget instance in the Lean file. -/
-  range? : Option Lsp.Range
-  deriving ToJson, FromJson
+structure PanelWidgetInstance extends WidgetInstance where
+  /-- The syntactic span in the Lean file at which the panel widget is displayed. -/
+  range? : Option Lsp.Range := none
+  /-- When present, the infoview will wrap the widget
+  in `<details><summary>{name}</summary>...</details>`.
+  This functionality is deprecated
+  but retained for backwards compatibility
+  with `UserWidgetDefinition`. -/
+  name? : Option String := none
+#mkrpcenc PanelWidgetInstance
 
 /-- Output of `getWidgets` RPC.-/
 structure GetWidgetsResponse where
-  widgets : Array UserWidgetInstance
-  deriving ToJson, FromJson
+  widgets : Array PanelWidgetInstance
+#mkrpcenc GetWidgetsResponse
 
 open Lean Server RequestM in
-/-- Get the `UserWidget`s present at a particular position. -/
+/-- Get the panel widgets present around a particular position. -/
 @[server_rpc_method]
-def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
+def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
   let doc ← readDoc
   let filemap := doc.meta.text
-  let pos := filemap.lspPosToUtf8Pos args
-  withWaitFindSnap doc (·.endPos >= pos) (notFoundX := return ⟨∅⟩) fun snap => do
-    let env := snap.env
-    let ws := widgetInfosAt? filemap snap.infoTree pos
-    let ws ← ws.toArray.mapM (fun (w : UserWidgetInfo) => do
-      let some widget := userWidgetRegistry.find? env w.widgetId
-        | throw <| RequestError.mk .invalidParams s!"No registered user-widget with id {w.widgetId}"
-      return {
-        widget with
-        props := w.props
-        range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx
-      })
-    return {widgets := ws}
+  let nextLine := { line := pos.line + 1, character := 0 }
+  let t := doc.cmdSnaps.waitUntil fun snap => filemap.lspPosToUtf8Pos nextLine ≤ snap.endPos
+  mapTask t fun (snaps, _) => do
+    let some snap := snaps.getLast?
+      | return ⟨∅⟩
+    runTermElabM snap do
+      let env ← getEnv
+      /- Panels from the environment. -/
+      let ws' ← evalPanelWidgets
+      let ws' : Array PanelWidgetInstance ← ws'.mapM fun wi => do
+        -- Check if the definition uses the deprecated `UserWidgetDefinition`
+        -- on a best-effort basis.
+        -- If it does, also send the `name` field.
+        let name? ← env.find? wi.id
+          |>.filter (·.type.isConstOf ``UserWidgetDefinition)
+          |>.mapM fun _ => do
+            let uwd ← evalUserWidgetDefinition wi.id
+            return uwd.name
+        return { wi with name? }
+      /- Panels from the infotree. -/
+      let ws := widgetInfosAt? filemap snap.infoTree pos.line
+      let ws : Array PanelWidgetInstance ← ws.toArray.mapM fun (wi : UserWidgetInfo) => do
+        let name? ← env.find? wi.id
+          |>.filter (·.type.isConstOf ``UserWidgetDefinition)
+          |>.mapM fun _ => do
+            let uwd ← evalUserWidgetDefinition wi.id
+            return uwd.name
+        return { wi with range? := String.Range.toLspRange filemap <$> Syntax.getRange? wi.stx, name? }
+      return { widgets := ws' ++ ws }
 
-/-- Save a user-widget instance to the infotree.
-    The given `widgetId` should be the declaration name of the widget definition. -/
-def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetId : Name) (props : Json) (stx : Syntax):  m Unit := do
-  let info := Info.ofUserWidgetInfo {
-    widgetId := widgetId
-    props := props
-    stx := stx
-  }
-  pushInfoLeaf info
-
-/-!  # Widget command -/
-
-/-- Use `#widget <widgetname> <props>` to display a widget. Useful for debugging widgets. -/
-syntax (name := widgetCmd) "#widget " ident ppSpace term : command
-
-open Lean Lean.Meta Lean.Elab Lean.Elab.Term in
-private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json :=
-  Lean.Elab.Term.evalTerm Json (mkConst ``Json) stx
-
-@[implemented_by evalJsonUnsafe]
-private opaque evalJson (stx : Syntax) : TermElabM Json
-
-open Elab Command in
-
-@[command_elab widgetCmd] def elabWidgetCmd : CommandElab := fun
-  | stx@`(#widget $id:ident $props) => do
-    let props : Json ← runTermElabM fun _ => evalJson props
-    saveWidgetInfo id.getId props stx
-  | _ => throwUnsupportedSyntax
+attribute [deprecated Module] UserWidgetDefinition
 
 end Lean.Widget

tests/lean/derivingRpcEncoding.lean

@@ -16,7 +16,6 @@ structure FooRef where
   a : Array Nat
   deriving Inhabited, TypeName
 
-#check instTypeNameFooRef
 #eval test (WithRpcRef FooRef) default
 
 structure FooJson where
@@ -28,21 +27,18 @@ structure Bar where
   fooJson : FooJson
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableBar
 #eval test Bar default
 
 structure BarTrans where
   bar : Bar
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableBarTrans
 #eval test BarTrans default
 
 structure Baz where
   arr : Array String -- non-constant field
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableBaz
 #eval test Baz default
 
 structure FooGeneric (α : Type) where
@@ -50,7 +46,6 @@ structure FooGeneric (α : Type) where
   b? : Option α
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableFooGeneric
 #eval test (FooGeneric Nat) default
 #eval test (FooGeneric Nat) { a := 3, b? := some 42 }
 
@@ -58,7 +53,6 @@ inductive BazInductive
   | baz (arr : Array Bar)
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableBazInductive
 #eval test BazInductive ⟨#[default, default]⟩
 
 inductive FooInductive (α : Type) where
@@ -66,7 +60,6 @@ inductive FooInductive (α : Type) where
   | b : (n : Nat) → (a : α) → (m : Nat) → FooInductive α
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableFooInductive
 #eval test (FooInductive BazInductive) (.a default default)
 #eval test (FooInductive BazInductive) (.b 42 default default)
 
@@ -80,20 +73,17 @@ inductive FooParam (n : Nat) where
   | a : Nat → FooParam n
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableFooParam
 #eval test (FooParam 10) (.a 42)
 
 inductive Unused (α : Type) | a
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableUnused
 structure NoRpcEncodable
 #eval test (Unused NoRpcEncodable) default
 
 structure UnusedStruct (α : Type)
   deriving RpcEncodable, Inhabited
 
-#check instRpcEncodableUnusedStruct
 #eval test (UnusedStruct NoRpcEncodable) default
 
 deriving instance Repr, RpcEncodable for Empty

tests/lean/derivingRpcEncoding.lean.expected.out

@@ -1,27 +1,17 @@
-instTypeNameFooRef : TypeName FooRef
 ok: {"p": "0"}
-instRpcEncodableBar : RpcEncodable Bar
 ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}
-instRpcEncodableBarTrans : RpcEncodable BarTrans
 ok: {"bar": {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}}
-instRpcEncodableBaz : RpcEncodable Baz
 ok: {"arr": []}
-instRpcEncodableFooGeneric {α : Type} [inst✝ : RpcEncodable α] : RpcEncodable (FooGeneric α)
 ok: {"a": 0}
 ok: {"b": 42, "a": 3}
-instRpcEncodableBazInductive : RpcEncodable BazInductive
 ok: {"baz":
  {"arr":
   [{"fooRef": {"p": "0"}, "fooJson": {"s": ""}},
    {"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}}
-instRpcEncodableFooInductive {α : Type} [inst✝ : RpcEncodable α] : RpcEncodable (FooInductive α)
 ok: {"a": [{"baz": {"arr": []}}, {"p": "0"}]}
 ok: {"b": {"n": 42, "m": 0, "a": {"baz": {"arr": []}}}}
 ok: {"a": [{"baz": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]}
-instRpcEncodableFooParam {n : Nat} : RpcEncodable (FooParam n)
 ok: {"a": 42}
-instRpcEncodableUnused {α : Type} : RpcEncodable (Unused α)
 ok: "a"
-instRpcEncodableUnusedStruct {α : Type} : RpcEncodable (UnusedStruct α)
 ok: {}
 Except.error "no inductive constructor matched"

tests/lean/interactive/run.lean

@@ -33,6 +33,30 @@ structure InteractiveGoals where
 
 end Client
 
+/-! Test-only instances -/
+
+instance : FromJson Widget.PanelWidgetInstance where
+  fromJson? j := do
+    let id ← j.getObjValAs? Name "id"
+    let javascriptHash ← j.getObjValAs? UInt64 "javascriptHash"
+    let props ← j.getObjVal? "props"
+    let range? ← j.getObjValAs? (Option Lsp.Range) "range"
+    return { id, javascriptHash, props := pure props, range? }
+
+deriving instance FromJson for Widget.GetWidgetsResponse
+
+def Lean.Widget.GetWidgetsResponse.debugJson (r : Widget.GetWidgetsResponse) : Json :=
+  Json.mkObj [
+    ("widgets", Json.arr (r.widgets.map fun w =>
+      Json.mkObj [
+        ("id", toJson w.id),
+        ("javascriptHash", toJson w.javascriptHash),
+        ("props", w.props.run' {}),
+        ("range", toJson w.range?),
+      ])
+    )
+  ]
+
 def word : Parsec String :=
   Parsec.many1Chars <| Parsec.digit <|> Parsec.asciiLetter <|> Parsec.pchar '_'
 
@@ -155,7 +179,7 @@ partial def main (args : List String) : IO Unit := do
           Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
           let response ← Ipc.readResponseAs requestNo Lean.Widget.GetWidgetsResponse
           requestNo := requestNo + 1
-          IO.eprintln (toJson response.result)
+          IO.eprintln response.result.debugJson
           for w in response.result.widgets do
             let params : Lean.Widget.GetWidgetSourceParams := { pos, hash := w.javascriptHash }
             let ps : RpcCallParams := {

tests/lean/interactive/userWidget.lean

@@ -1,15 +1,38 @@
 import Lean
-open Lean Widget
+open Lean
 
-@[widget]
-def widget1 : UserWidgetDefinition := {
-  name := "my fancy widget"
-  javascript:= "
-  import * as React from 'react';
-  export default function (props) {
-    return React.createElement('p', {}, 'hello')
-  }"
-}
+@[widget_module]
+def helloWidget : Widget.Module where
+  javascript := "
+    import * as React from 'react';
+    export default function(props) {
+      const name = props.name || 'world'
+      return React.createElement('p', {}, name + '!')
+    }"
 
-#widget widget1 (Json.mkObj [])
+#widget helloWidget
   --^ widgets
+
+structure HelloWidgetProps where
+  name? : Option String := none
+  deriving Server.RpcEncodable
+
+#widget helloWidget with { name? := "lean" : HelloWidgetProps }
+  --^ widgets
+
+show_panel_widgets [helloWidget with { name? := "global" : HelloWidgetProps }]
+
+section
+show_panel_widgets [local helloWidget with { name? := "local" : HelloWidgetProps }]
+--^ widgets
+end
+
+namespace Foo
+show_panel_widgets [scoped helloWidget with { name? := "scoped" : HelloWidgetProps }]
+end Foo
+
+open scoped Foo
+--^ widgets
+
+show_panel_widgets [-helloWidget]
+--^ widgets

tests/lean/interactive/userWidget.lean.expected.out

@@ -1,10 +1,45 @@
 {"widgets":
  [{"range":
-   {"start": {"line": 13, "character": 0},
-    "end": {"line": 13, "character": 31}},
+   {"start": {"line": 12, "character": 0},
+    "end": {"line": 12, "character": 19}},
    "props": {},
-   "name": "my fancy widget",
-   "javascriptHash": "11948876261158841348",
-   "id": "widget1"}]}
+   "javascriptHash": "2874772427606622741",
+   "id": "helloWidget"}]}
 {"sourcetext":
- "\n  import * as React from 'react';\n  export default function (props) {\n    return React.createElement('p', {}, 'hello')\n  }"}
+ "\n    import * as React from 'react';\n    export default function(props) {\n      const name = props.name || 'world'\n      return React.createElement('p', {}, name + '!')\n    }"}
+{"widgets":
+ [{"range":
+   {"start": {"line": 19, "character": 0},
+    "end": {"line": 19, "character": 63}},
+   "props": {"name": "lean"},
+   "javascriptHash": "2874772427606622741",
+   "id": "helloWidget"}]}
+{"sourcetext":
+ "\n    import * as React from 'react';\n    export default function(props) {\n      const name = props.name || 'world'\n      return React.createElement('p', {}, name + '!')\n    }"}
+{"widgets":
+ [{"range": null,
+   "props": {"name": "local"},
+   "javascriptHash": "2874772427606622741",
+   "id": "helloWidget"},
+  {"range": null,
+   "props": {"name": "global"},
+   "javascriptHash": "2874772427606622741",
+   "id": "helloWidget"}]}
+{"sourcetext":
+ "\n    import * as React from 'react';\n    export default function(props) {\n      const name = props.name || 'world'\n      return React.createElement('p', {}, name + '!')\n    }"}
+{"sourcetext":
+ "\n    import * as React from 'react';\n    export default function(props) {\n      const name = props.name || 'world'\n      return React.createElement('p', {}, name + '!')\n    }"}
+{"widgets":
+ [{"range": null,
+   "props": {"name": "scoped"},
+   "javascriptHash": "2874772427606622741",
+   "id": "helloWidget"},
+  {"range": null,
+   "props": {"name": "global"},
+   "javascriptHash": "2874772427606622741",
+   "id": "helloWidget"}]}
+{"sourcetext":
+ "\n    import * as React from 'react';\n    export default function(props) {\n      const name = props.name || 'world'\n      return React.createElement('p', {}, name + '!')\n    }"}
+{"sourcetext":
+ "\n    import * as React from 'react';\n    export default function(props) {\n      const name = props.name || 'world'\n      return React.createElement('p', {}, name + '!')\n    }"}
+{"widgets": []}