@[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 : Std.TreeMap UInt64 (Lean.Name × Lean.Widget.Module) compare) => x.insert m.javascriptHash.val (id, m)

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.instToJsonGetWidgetSourceParams.toJson }

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

Equations

• Lean.Widget.instToJsonGetWidgetSourceParams.toJson x✝ = Lean.Json.mkObj [[("hash", Lean.toJson x✝.hash)], [("pos", Lean.toJson x✝.pos)]].flatten

instance Lean.Widget.instFromJsonGetWidgetSourceParams : FromJson GetWidgetSourceParams

Equations

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

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

Equations

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

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 := Lean.Widget.instInhabitedWidgetSource.default }

def Lean.Widget.instInhabitedWidgetSource.default : WidgetSource

Equations

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

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

Equations

• Lean.Widget.instToJsonWidgetSource.toJson x✝ = Lean.Json.mkObj [[("sourcetext", Lean.toJson x✝.sourcetext)]].flatten

instance Lean.Widget.instToJsonWidgetSource : ToJson WidgetSource

Equations

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

instance Lean.Widget.instFromJsonWidgetSource : FromJson WidgetSource

Equations

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

def Lean.Widget.instFromJsonWidgetSource.fromJson : Json → Except String WidgetSource

Equations

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

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

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.

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

Equations

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

instance Lean.Widget.instInhabitedUserWidgetDefinition : Inhabited UserWidgetDefinition

Equations

• Lean.Widget.instInhabitedUserWidgetDefinition = { default := Lean.Widget.instInhabitedUserWidgetDefinition.default }

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

Equations

• Lean.Widget.instToJsonUserWidgetDefinition.toJson x✝ = Lean.Json.mkObj [[("name", Lean.toJson x✝.name)], [("javascript", Lean.toJson x✝.javascript)]].flatten

instance Lean.Widget.instToJsonUserWidgetDefinition : ToJson UserWidgetDefinition

Equations

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

instance Lean.Widget.instFromJsonUserWidgetDefinition : FromJson UserWidgetDefinition

Equations

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

def Lean.Widget.instFromJsonUserWidgetDefinition.fromJson : Json → Except String UserWidgetDefinition

Equations

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

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.