structure Lean.Widget.WidgetSource : Type

• sourcetext : String

  Sourcetext of the code to run.

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.

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

• name : String

  Pretty name of user widget to display to the user.

• javascript : String

  An ESmodule that exports a react component to render.

Use this structure and the @[widget] attribute to define your own widgets.

@[widget]
def rubiks : UserWidgetDefinition :=
  { name := "Rubiks cube app"
    javascript := include_str ...
  }

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

• hash : UInt64

  The hash of the sourcetext to retrieve.

• pos : Lean.Lsp.Position

Input for getWidgetSource RPC.

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

• 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.

UserWidget accompanied by component props.

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

• widgets : Array Lean.Widget.UserWidgetInstance

Output of getWidgets RPC.

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