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

def Lean.Widget.instToJsonGetWidgetSourceParams.toJson : GetWidgetSourceParams → Json

instance Lean.Widget.instFromJsonGetWidgetSourceParams : FromJson GetWidgetSourceParams

def Lean.Widget.instFromJsonGetWidgetSourceParams.fromJson : Json → Except String GetWidgetSourceParams

structure Lean.Widget.WidgetSource : Type

• sourcetext : String

  Sourcetext of the JS module to run.

instance Lean.Widget.instInhabitedWidgetSource : Inhabited WidgetSource

def Lean.Widget.instInhabitedWidgetSource.default : WidgetSource

def Lean.Widget.instToJsonWidgetSource.toJson : WidgetSource → Json

instance Lean.Widget.instToJsonWidgetSource : ToJson WidgetSource

instance Lean.Widget.instFromJsonWidgetSource : FromJson WidgetSource

def Lean.Widget.instFromJsonWidgetSource.fromJson : Json → Except String 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

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.

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.

def Lean.Widget.instInhabitedUserWidgetDefinition.default : UserWidgetDefinition

instance Lean.Widget.instInhabitedUserWidgetDefinition : Inhabited UserWidgetDefinition

def Lean.Widget.instToJsonUserWidgetDefinition.toJson : UserWidgetDefinition → Json

instance Lean.Widget.instToJsonUserWidgetDefinition : ToJson UserWidgetDefinition

instance Lean.Widget.instFromJsonUserWidgetDefinition : FromJson UserWidgetDefinition

def Lean.Widget.instFromJsonUserWidgetDefinition.fromJson : Json → Except String 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.