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

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

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

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

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

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

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

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

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

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

instance Lean.Widget.instFromJsonGetWidgetSourceParams : Lean.FromJson Lean.Widget.GetWidgetSourceParams

def Lean.Widget.getWidgetSource (args : Lean.Widget.GetWidgetSourceParams) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Widget.WidgetSource)

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.

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

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

structure Lean.Widget.GetWidgetsResponse : Type

• widgets : Array Lean.Widget.UserWidgetInstance

Output of getWidgets RPC.

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

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

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.

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.

Widget command

def Lean.Widget.widgetCmd : Lean.ParserDescr

Use #widget to display a widget. Useful for debugging widgets.

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