- 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.
Instances For
- 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 ...
}
Instances For
- hash : UInt64
The hash of the sourcetext to retrieve.
- pos : Lean.Lsp.Position
Input for getWidgetSource
RPC.
Instances For
Try to retrieve the UserWidgetInfo
at a particular position.
Instances For
Get the UserWidget
s present at a particular position.
Instances For
Save a user-widget instance to the infotree.
The given widgetId
should be the declaration name of the widget definition.
Instances For
Widget command #
Use #widget
to display a widget. Useful for debugging widgets.