def ProofWidgets.ofRpcMethodTemplate : String

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.«termMk_rpc_widget%_» : Lean.ParserDescr

The elaborator mk_rpc_widget% allows writing certain widgets in Lean instead of JavaScript. Specifically, it translates an RPC method of type MyProps → RequestM (RequestTask Html) into a widget component of type Component MyProps.

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.

⚠️ However, note that there are several limitations on what such component can do compared to ones written natively in TypeScript or JavaScript:

• 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 <button onClick={..}> child.
• 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. Given 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 #[]

Equations

• One or more equations did not get rendered due to their size.