source
structure Lean.Widget.WidgetInstance :
Type

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.

- props : StateM Server.RpcObjectStore Json

  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

source
instance Lean.Widget.instRpcEncodableWidgetInstance :
Server.RpcEncodable WidgetInstance
Equations

- Lean.Widget.instRpcEncodableWidgetInstance = { rpcEncode := Lean.Widget.instRpcEncodableWidgetInstance.enc✝, rpcDecode := Lean.Widget.instRpcEncodableWidgetInstance.dec✝ }

source
structure Lean.Widget.Module :
Type

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