Documentation

Lean.Widget.Types

An instance of a widget component: the identifier of a widget module and the hash of its JS source code together with props.

See the manual entry for more information about widgets.

  • id : Name

    Name of the @[widget_module].

  • javascriptHash : UInt64

    Hash of the JS source of the widget module.

  • Arguments to be passed to the component's default exported function. Must be a JSON object.

    In certain contexts (such as when rendering as a panel widget; see Widget.savePanelWidgetInfo), the Lean infoview appends additional fields to this object.

    Props may contain RPC references, so must be stored as a StateM computation with access to the RPC object store.

Instances For

    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