structure Lean.Widget.WidgetSource : Type

A custom piece of code that is run on the editor client.

The editor can use the Lean.Widget.getWidgetSource RPC method to get this object.

See the manual entry above this declaration for more information on how to use the widgets system.

• sourcetext : String

  Sourcetext of the code 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✝ }

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✝ }

structure Lean.Widget.UserWidget : Type

• id : Lake.Name
• name : String

  Pretty name of widget to display to the user.

• javascriptHash : UInt64

instance Lean.Widget.instInhabitedUserWidget : Inhabited Lean.Widget.UserWidget

Equations

• Lean.Widget.instInhabitedUserWidget = { default := { id := default, name := default, javascriptHash := default } }

instance Lean.Widget.instToJsonUserWidget : Lean.ToJson Lean.Widget.UserWidget

Equations

• Lean.Widget.instToJsonUserWidget = { toJson := Lean.Widget.toJsonUserWidget✝ }

instance Lean.Widget.instFromJsonUserWidget : Lean.FromJson Lean.Widget.UserWidget

Equations

• Lean.Widget.instFromJsonUserWidget = { fromJson? := Lean.Widget.fromJsonUserWidget✝ }

opaque Lean.Widget.userWidgetRegistry : Lean.MapDeclarationExtension Lean.Widget.UserWidget

opaque Lean.Widget.widgetSourceRegistry : Lean.Widget.WidgetSourceRegistry

structure Lean.Widget.GetWidgetSourceParams : Type

Input for getWidgetSource RPC.

• hash : UInt64

  The hash of the sourcetext 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✝ }

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.

def Lean.Widget.widgetInfosAt? (text : Lean.FileMap) (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) : List Lean.Elab.UserWidgetInfo

Try to retrieve the UserWidgetInfo at a particular position.

Equations

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

structure Lean.Widget.UserWidgetInstanceextends Lean.Widget.UserWidget : Type

UserWidget accompanied by component props.

• id : Lake.Name
• name : String
• javascriptHash : UInt64
• props : Lean.Json

  Arguments to be fed to the widget's main component.

• range? : Option Lean.Lsp.Range

  The location of the widget instance in the Lean file.

instance Lean.Widget.instToJsonUserWidgetInstance : Lean.ToJson Lean.Widget.UserWidgetInstance

Equations

• Lean.Widget.instToJsonUserWidgetInstance = { toJson := Lean.Widget.toJsonUserWidgetInstance✝ }

instance Lean.Widget.instFromJsonUserWidgetInstance : Lean.FromJson Lean.Widget.UserWidgetInstance

Equations

• Lean.Widget.instFromJsonUserWidgetInstance = { fromJson? := Lean.Widget.fromJsonUserWidgetInstance✝ }

structure Lean.Widget.GetWidgetsResponse : Type

Output of getWidgets RPC.

• widgets : Array Lean.Widget.UserWidgetInstance

instance Lean.Widget.instToJsonGetWidgetsResponse : Lean.ToJson Lean.Widget.GetWidgetsResponse

Equations

• Lean.Widget.instToJsonGetWidgetsResponse = { toJson := Lean.Widget.toJsonGetWidgetsResponse✝ }

instance Lean.Widget.instFromJsonGetWidgetsResponse : Lean.FromJson Lean.Widget.GetWidgetsResponse

Equations

• Lean.Widget.instFromJsonGetWidgetsResponse = { fromJson? := Lean.Widget.fromJsonGetWidgetsResponse✝ }

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

Get the UserWidgets present at a particular position.

Equations

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

def Lean.Widget.saveWidgetInfo {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.Elab.MonadInfoTree m] (widgetId : Lake.Name) (props : Lean.Json) (stx : Lean.Syntax) : m Unit

Save a user-widget instance to the infotree. The given widgetId should be the declaration name of the widget definition.

Equations

• Lean.Widget.saveWidgetInfo widgetId props stx = let info := Lean.Elab.Info.ofUserWidgetInfo { stx := stx, widgetId := widgetId, props := props }; Lean.Elab.pushInfoLeaf info

Widget command

def Lean.Widget.widgetCmd : Lean.ParserDescr

Use #widget <widgetname> <props> to display a widget. Useful for debugging widgets.

Equations

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

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

Equations

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