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.

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, javascriptHash := ⟨hash 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.