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
Equations
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
andreact
.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. The hash is cached to avoid recomputing it whenever the
Module
is used.