structure Lean.Widget.Module : Type

A widget module is a unit of source code that can execute in the infoview.

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 for more information on how to use the widgets system.

• javascript : String

  A JS module 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 and 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.

• javascriptHash : { x : UInt64 // x = hash self.javascript }

  The hash is cached to avoid recomputing it whenever the Module is used.

@[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

Equations

• Lean.Widget.instToModuleModule = { toModule := id }

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

Equations

• Lean.Widget.addBuiltinModule id m = ST.Ref.modify Lean.Widget.builtinModulesRef✝ fun (x : Lean.RBMap UInt64 (Lean.Name × Lean.Widget.Module) compare) => x.insert m.javascriptHash.val (id, m)

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

Equations

• Lean.Widget.instToJsonGetWidgetSourceParams = { toJson := Lean.Widget.toJsonGetWidgetSourceParams✝ }

instance Lean.Widget.instFromJsonGetWidgetSourceParams : FromJson GetWidgetSourceParams

Equations

• Lean.Widget.instFromJsonGetWidgetSourceParams = { fromJson? := Lean.Widget.fromJsonGetWidgetSourceParams✝ }

structure Lean.Widget.WidgetSource : Type

• sourcetext : String

  Sourcetext of the JS module to run.

instance Lean.Widget.instInhabitedWidgetSource : Inhabited WidgetSource

Equations

• Lean.Widget.instInhabitedWidgetSource = { default := { sourcetext := default } }

instance Lean.Widget.instToJsonWidgetSource : ToJson WidgetSource

Equations

• Lean.Widget.instToJsonWidgetSource = { toJson := Lean.Widget.toJsonWidgetSource✝ }

instance Lean.Widget.instFromJsonWidgetSource : FromJson WidgetSource

Equations

• Lean.Widget.instFromJsonWidgetSource = { fromJson? := Lean.Widget.fromJsonWidgetSource✝ }

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Widget.addPanelWidgetGlobal h n = Lean.ScopedEnvExtension.add Lean.Widget.panelWidgetsExt (h, n)

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

Equations

• Lean.Widget.addPanelWidgetScoped h n = Lean.ScopedEnvExtension.add Lean.Widget.panelWidgetsExt (h, n) Lean.AttributeKind.scoped

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

show_panel_widgets command

def Lean.Widget.widgetInstanceSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Widget.addWidgetSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Widget.eraseWidgetSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Widget.showWidgetSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

#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.

Equations

• Lean.Widget.widgetCmd = Lean.ParserDescr.node `Lean.Widget.widgetCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#widget ") Lean.Widget.widgetInstanceSpec)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Widget.instInhabitedUserWidgetDefinition = { default := { name := default, javascript := default } }

instance Lean.Widget.instToJsonUserWidgetDefinition : ToJson UserWidgetDefinition

Equations

• Lean.Widget.instToJsonUserWidgetDefinition = { toJson := Lean.Widget.toJsonUserWidgetDefinition✝ }

instance Lean.Widget.instFromJsonUserWidgetDefinition : FromJson UserWidgetDefinition

Equations

• Lean.Widget.instFromJsonUserWidgetDefinition = { fromJson? := Lean.Widget.fromJsonUserWidgetDefinition✝ }

instance Lean.Widget.instToModuleUserWidgetDefinition : ToModule UserWidgetDefinition

Equations

• Lean.Widget.instToModuleUserWidgetDefinition = { toModule := fun (uwd : Lean.Widget.UserWidgetDefinition) => { javascript := uwd.javascript } }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Widget.instRpcEncodablePanelWidgetInstance = { rpcEncode := Lean.Widget.instRpcEncodablePanelWidgetInstance.enc✝, rpcDecode := Lean.Widget.instRpcEncodablePanelWidgetInstance.dec✝ }

structure Lean.Widget.GetWidgetsResponse : Type

Output of getWidgets RPC.

• widgets : Array PanelWidgetInstance

instance Lean.Widget.instRpcEncodableGetWidgetsResponse : Server.RpcEncodable GetWidgetsResponse

Equations

• Lean.Widget.instRpcEncodableGetWidgetsResponse = { rpcEncode := Lean.Widget.instRpcEncodableGetWidgetsResponse.enc✝, rpcDecode := Lean.Widget.instRpcEncodableGetWidgetsResponse.dec✝ }

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

Get the panel widgets present around a particular position.

Equations

• One or more equations did not get rendered due to their size.