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

    def rubiks : UserWidgetDefinition :=
      { name := "Rubiks cube app"
        javascript := include_str ...
    Instances For
      Instances For

        Input for getWidgetSource RPC.

        Instances For

          Try to retrieve the UserWidgetInfo at a particular position.

          Instances For

            UserWidget accompanied by component props.

            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.

                Instances For