We define a representation of HTML trees including widget components.

inductive ProofWidgets.Html : Type

A HTML tree which may contain widget components.

• element : String → Array (String × Lean.Json) → Array Html → Html

  An element "tag" attrs children represents <tag {...attrs}>{...children}</tag>.

• text : String → Html

  Raw HTML text.

• component : UInt64 → String → LazyEncodable Lean.Json → Array Html → Html

  A component h e props children represents <Foo {...props}>{...children}</Foo>, where Foo : Component Props is some component such that h = hash Foo.javascript, e = Foo.«export», and props will produce a JSON-encoded value of type Props.

@[instance_reducible]

instance ProofWidgets.instInhabitedHtml : Inhabited Html

Equations

• ProofWidgets.instInhabitedHtml = { default := ProofWidgets.instInhabitedHtml.default }

@[instance_reducible]

instance ProofWidgets.instRpcEncodableHtml : Lean.Server.RpcEncodable Html

Equations

• ProofWidgets.instRpcEncodableHtml = { rpcEncode := ProofWidgets.instRpcEncodableHtml.enc✝, rpcDecode := ProofWidgets.instRpcEncodableHtml.dec✝ }

def ProofWidgets.Html.ofComponent {Props : Type} [Lean.Server.RpcEncodable Props] (c : Component Props) (props : Props) (children : Array Html) : Html

Equations

• ProofWidgets.Html.ofComponent c props children = ProofWidgets.Html.component (hash c.javascript) c.export (Lean.Server.rpcEncode props) children

inductive ProofWidgets.LayoutKind : Type

See MDN docs.

• block : LayoutKind
• inline : LayoutKind