@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalModuleUnsafe]

opaque Lean.Widget.evalModule (e : Expr) : MetaM Module

@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalWidgetInstanceUnsafe]

opaque Lean.Widget.evalWidgetInstance (e : Expr) : MetaM WidgetInstance

Storage of widget modules

class Lean.Widget.ToModule (α : Type u) : Type u

• toModule : α → Module

instance Lean.Widget.instToModuleModule : ToModule Module

def Lean.Widget.addBuiltinModule (id : Name) (m : Module) : IO Unit

opaque Lean.Widget.moduleRegistry : Lean.Widget.ModuleRegistry✝

opaque Lean.Widget.widgetModuleAttrImpl : AttributeImpl

Registers a widget module. Its type must implement Lean.Widget.ToModule.

Retrieval of widget modules

structure Lean.Widget.GetWidgetSourceParams : Type

• hash : UInt64

  Hash of the JS module to retrieve.

• pos : Lsp.Position

instance Lean.Widget.instToJsonGetWidgetSourceParams : ToJson GetWidgetSourceParams

instance Lean.Widget.instFromJsonGetWidgetSourceParams : FromJson GetWidgetSourceParams

structure Lean.Widget.WidgetSource : Type

• sourcetext : String

  Sourcetext of the JS module to run.

instance Lean.Widget.instInhabitedWidgetSource : Inhabited WidgetSource

instance Lean.Widget.instToJsonWidgetSource : ToJson WidgetSource

instance Lean.Widget.instFromJsonWidgetSource : FromJson WidgetSource

def Lean.Widget.getWidgetSource (args : GetWidgetSourceParams) : Server.RequestM (Server.RequestTask WidgetSource)

Storage of panel widget instances

inductive Lean.Widget.PanelWidgetsExtEntry : Type

• global (n : Name) : PanelWidgetsExtEntry
• local (wi : WidgetInstance) : PanelWidgetsExtEntry

opaque Lean.Widget.panelWidgetsExt : Lean.Widget.PanelWidgetsExt✝

def Lean.Widget.evalPanelWidgets : MetaM (Array WidgetInstance)

def Lean.Widget.addPanelWidgetGlobal {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit

def Lean.Widget.addPanelWidgetScoped {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit

def Lean.Widget.addPanelWidgetLocal {m : Type → Type} [Monad m] [MonadEnv m] (wi : WidgetInstance) : m Unit

def Lean.Widget.erasePanelWidget {m : Type → Type} [Monad m] [MonadEnv m] (h : UInt64) : m Unit

def Lean.Widget.WidgetInstance.ofHash (hash : UInt64) (props : StateM Server.RpcObjectStore Json) : CoreM WidgetInstance

Construct a widget instance by finding a widget module in the current environment.

hash must be hash (toModule c).javascript where c is some global constant annotated with @[widget_module], or the name of a builtin widget module.

def Lean.Widget.savePanelWidgetInfo (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) : CoreM Unit

Save the data of a panel widget which will be displayed whenever the text cursor is on stx.

hash must be as in WidgetInstance.ofHash.

For panel widgets, the Lean infoview appends additional fields to the props object: see https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/userWidget.tsx#L145.

show_panel_widgets command

def Lean.Widget.widgetInstanceSpec : ParserDescr

def Lean.Widget.elabWidgetInstanceSpecAux (mod : Ident) (props : Term) : Elab.TermElabM Expr

def Lean.Widget.elabWidgetInstanceSpec : TSyntax `Lean.Widget.widgetInstanceSpec → Elab.TermElabM Expr

def Lean.Widget.addWidgetSpec : ParserDescr

def Lean.Widget.eraseWidgetSpec : ParserDescr

def Lean.Widget.showWidgetSpec : ParserDescr

def Lean.Widget.showPanelWidgetsCmd : ParserDescr

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.

def Lean.Widget.elabShowPanelWidgetsCmd : Elab.Command.CommandElab

#widget command

def Lean.Widget.widgetCmd : ParserDescr

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.

def Lean.Widget.elabWidgetCmd : Elab.Command.CommandElab

Deprecated definitions

structure Lean.Widget.UserWidgetDefinition : Type

Use this structure and the @[widget] attribute to define your own widgets.

@[widget]
def rubiks : UserWidgetDefinition :=
  { name := "Rubiks cube app"
    javascript := include_str ...
  }

• name : String

  Pretty name of user widget to display to the user.

• javascript : String

  An ESmodule that exports a react component to render.

instance Lean.Widget.instInhabitedUserWidgetDefinition : Inhabited UserWidgetDefinition

instance Lean.Widget.instToJsonUserWidgetDefinition : ToJson UserWidgetDefinition

instance Lean.Widget.instFromJsonUserWidgetDefinition : FromJson UserWidgetDefinition

instance Lean.Widget.instToModuleUserWidgetDefinition : ToModule UserWidgetDefinition

@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalUserWidgetDefinitionUnsafe]

opaque Lean.Widget.evalUserWidgetDefinition {m : Type → Type} [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m] (id : Name) : m UserWidgetDefinition

Retrieving panel widget instances

def Lean.Widget.widgetInfosAt? (text : FileMap) (t : Elab.InfoTree) (hoverLine : Nat) : List Elab.UserWidgetInfo

Retrieve all the UserWidgetInfos that intersect a given line.

structure Lean.Widget.PanelWidgetInstanceextends Lean.Widget.WidgetInstance : Type

• id : Name
• javascriptHash : UInt64
• props : StateM Server.RpcObjectStore Json
• range? : Option Lsp.Range

  The syntactic span in the Lean file at which the panel widget is displayed.

• name? : Option String

  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.

instance Lean.Widget.instRpcEncodablePanelWidgetInstance : Server.RpcEncodable PanelWidgetInstance

structure Lean.Widget.GetWidgetsResponse : Type

Output of getWidgets RPC.

• widgets : Array PanelWidgetInstance

instance Lean.Widget.instRpcEncodableGetWidgetsResponse : Server.RpcEncodable GetWidgetsResponse

def Lean.Widget.getWidgets (pos : Lsp.Position) : Server.RequestM (Server.RequestTask GetWidgetsResponse)

Get the panel widgets present around a particular position.