Specifically, it translates an RPC method of type
MyProps → RequestM (RequestTask Html)
into a widget component of type
Even more specifically, we can write:
open Lean Server structure MyProps where ... deriving RpcEncodable @[server_rpc_method] def MyComponent.rpc (ps : MyProps) : RequestM (RequestTask Html) := ... @[widget_module] def MyComponent : Component MyProps := mk_rpc_widget% MyComponent.rpc
This is convenient because we can program the logic that computes an output HTML tree given input props in Lean directly.
- It must be pure, i.e. cannot directly store any React state. Child components may store state as usual.
- It cannot pass closures as props to the child components that it returns.
For example, it is not currently possible to write click event handlers in Lean
and pass them to a
- Every time the input props change, the infoview has to send a message to the Lean server in order to invoke the RPC method. Thus there can be a noticeable visual delay between the input props changing and the display updating. Consequently, components whose props change at a high frequency (e.g. depending on the mouse position) should not be implemented using this method.
💡 Note that an inverse transformation is already possible.
MyComponent : Component MyProps, we can write:
open Lean Server @[server_rpc_method] def MyComponent.rpc (ps : MyProps) : RequestM (RequestTask Html) := RequestM.asTask do return Html.ofComponent MyComponent ps #
- One or more equations did not get rendered due to their size.