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