Documentation

Lean.Widget.UserWidget

A widget module is a unit of source code that can execute in the infoview.

Every module definition must either be annotated with @[widget_module], or use a value of javascript identical to that of another definition annotated with @[widget_module]. This makes it possible for the infoview to load the module.

See the manual entry for more information on how to use the widgets system.

  • javascript : String

    A JS module intended for use in user widgets.

    The JS environment in which modules execute provides a fixed set of libraries accessible via direct import, notably @leanprover/infoview and react.

    To initialize this field from an external JS file, you may use include_str "path"/"to"/"file.js". However beware that this does not register a dependency with Lake, so your Lean module will not automatically be rebuilt when the .js file changes.

  • javascriptHash : { x : UInt64 // x = hash self.javascript }

    The hash is cached to avoid recomputing it whenever the Module is used.

Instances For
@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalModuleUnsafe]
@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalWidgetInstanceUnsafe]

Storage of widget modules #

Registers a widget module. Its type must implement Lean.Widget.ToModule.

Retrieval of widget modules #

Storage of panel widget instances #

Equations
  • One or more equations did not get rendered due to their size.

Construct a widget instance by finding a widget module in the current environment.

hash must be hash (toModule c).javascript where c is some global constant annotated with @[widget_module], or the name of a builtin widget module.

Save the data of a panel widget which will be displayed whenever the text cursor is on stx.

hash must be as in WidgetInstance.ofHash.

Equations
  • One or more equations did not get rendered due to their size.

show_panel_widgets command #

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

Use show_panel_widgets [<widget>] to mark that <widget> should always be displayed, including in downstream modules.

The type of <widget> must implement Widget.ToModule, and the type of <props> must implement Server.RpcEncodable. In particular, <props> : Json works.

Use show_panel_widgets [<widget> with <props>] to specify the <props> that the widget should be given as arguments.

Use show_panel_widgets [local <widget> (with <props>)?] to mark it for display in the current section, namespace, or file only.

Use show_panel_widgets [scoped <widget> (with <props>)?] to mark it for display only when the current namespace is open.

Use show_panel_widgets [-<widget>] to temporarily hide a previously shown widget in the current section, namespace, or file. Note that persistent erasure is not possible, i.e., -<widget> has no effect on downstream modules.

Equations
  • One or more equations did not get rendered due to their size.

#widget command #

Use #widget <widget> to display a panel widget, and #widget <widget> with <props> to display it with the given props. Useful for debugging widgets.

The type of <widget> must implement Widget.ToModule, and the type of <props> must implement Server.RpcEncodable. In particular, <props> : Json works.

Equations
Equations
  • One or more equations did not get rendered due to their size.

Deprecated definitions #

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

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

    Pretty name of user widget to display to the user.

  • javascript : String

    An ESmodule that exports a react component to render.

Instances For
@[implemented_by _private.Lean.Widget.UserWidget.0.Lean.Widget.evalUserWidgetDefinitionUnsafe]

Retrieving panel widget instances #

Retrieve all the UserWidgetInfos that intersect a given line.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

Get the panel widgets present around a particular position.

Equations
  • One or more equations did not get rendered due to their size.