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.

instance Lean.Widget.instRpcEncodableWidgetInstance : Server.RpcEncodable WidgetInstance

Equations

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