Documentation

Lean.Widget.UserWidget

@[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 #

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

Storage of panel widget instances #

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

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

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.

For panel widgets, the Lean infoview appends additional fields to the props object: see https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/userWidget.tsx#L145.

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.
def Lean.Widget.elabWidgetInstanceSpec :
TSyntax `Lean.Widget.widgetInstanceSpecElab.TermElabM Expr
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.
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.
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.