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 : Lean.Expr) : Lean.MetaM Lean.Widget.Module

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

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

Storage of widget modules

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

• toModule : α → Lean.Widget.Module

instance Lean.Widget.instToModuleModule : Lean.Widget.ToModule Lean.Widget.Module

Equations

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

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

Equations

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

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

opaque Lean.Widget.widgetModuleAttrImpl : Lean.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 : Lean.Lsp.Position

instance Lean.Widget.instToJsonGetWidgetSourceParams : Lean.ToJson Lean.Widget.GetWidgetSourceParams

Equations

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

instance Lean.Widget.instFromJsonGetWidgetSourceParams : Lean.FromJson Lean.Widget.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 Lean.Widget.WidgetSource

Equations

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

instance Lean.Widget.instToJsonWidgetSource : Lean.ToJson Lean.Widget.WidgetSource

Equations

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

instance Lean.Widget.instFromJsonWidgetSource : Lean.FromJson Lean.Widget.WidgetSource

Equations

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

def Lean.Widget.getWidgetSource (args : Lean.Widget.GetWidgetSourceParams) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Widget.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: Lake.Name → Lean.Widget.PanelWidgetsExtEntry
• local: Lean.Widget.WidgetInstance → Lean.Widget.PanelWidgetsExtEntry

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

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

Equations

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

def Lean.Widget.addPanelWidgetGlobal {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadResolveName m] (h : UInt64) (n : Lake.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] [Lean.MonadEnv m] [Lean.MonadResolveName m] (h : UInt64) (n : Lake.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] [Lean.MonadEnv m] (wi : Lean.Widget.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] [Lean.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 Lean.Server.RpcObjectStore Lean.Json) : Lean.CoreM Lean.Widget.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 Lean.Server.RpcObjectStore Lean.Json) (stx : Lean.Syntax) : Lean.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 : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

def Lean.Widget.addWidgetSpec : Lean.ParserDescr

Equations

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

def Lean.Widget.eraseWidgetSpec : Lean.ParserDescr

Equations

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

def Lean.Widget.showWidgetSpec : Lean.ParserDescr

Equations

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

def Lean.Widget.showPanelWidgetsCmd : Lean.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 : Lean.Elab.Command.CommandElab

Equations

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

#widget command

def Lean.Widget.widgetCmd : Lean.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 : Lean.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 Lean.Widget.UserWidgetDefinition

Equations

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

instance Lean.Widget.instToJsonUserWidgetDefinition : Lean.ToJson Lean.Widget.UserWidgetDefinition

Equations

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

instance Lean.Widget.instFromJsonUserWidgetDefinition : Lean.FromJson Lean.Widget.UserWidgetDefinition

Equations

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

instance Lean.Widget.instToModuleUserWidgetDefinition : Lean.Widget.ToModule Lean.Widget.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] [Lean.MonadEnv m] [Lean.MonadOptions m] [Lean.MonadError m] (id : Lake.Name) : m Lean.Widget.UserWidgetDefinition

Retrieving panel widget instances

def Lean.Widget.widgetInfosAt? (text : Lean.FileMap) (t : Lean.Elab.InfoTree) (hoverLine : Nat) : List Lean.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 : Lake.Name
• javascriptHash : UInt64
• props : StateM Lean.Server.RpcObjectStore Lean.Json
• range? : Option Lean.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 : Lean.Server.RpcEncodable Lean.Widget.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 Lean.Widget.PanelWidgetInstance

instance Lean.Widget.instRpcEncodableGetWidgetsResponse : Lean.Server.RpcEncodable Lean.Widget.GetWidgetsResponse

Equations

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

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

Get the panel widgets present around a particular position.

Equations

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