We define a representation of HTML trees together with a JSX-like DSL for writing them.

inductive ProofWidgets.Html : Type

A HTML tree which may contain widget components.

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

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

• text: String → ProofWidgets.Html

  Raw HTML text.

• component: UInt64 → String → ProofWidgets.LazyEncodable Lean.Json → Array ProofWidgets.Html → ProofWidgets.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 ProofWidgets.instInhabitedHtml : Inhabited ProofWidgets.Html

Equations

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

instance ProofWidgets.ProofWidgets.Html.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.ProofWidgets.Html.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.Html.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.ProofWidgets.Html.toJsonRpcEncodablePacket✝ }

instance ProofWidgets.ProofWidgets.Html.instRpcEncodableHtml : Lean.Server.RpcEncodable ProofWidgets.Html

Equations

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

instance ProofWidgets.ProofWidgets.Html.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.ProofWidgets.Html.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.Html.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.ProofWidgets.Html.fromJsonRpcEncodablePacket✝ }

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

Equations

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

inductive ProofWidgets.LayoutKind : Type

See MDN docs.

• block: ProofWidgets.LayoutKind
• inline: ProofWidgets.LayoutKind

def Lean.Parser.Category.jsxElement : Lean.Parser.Category

Equations

• Lean.Parser.Category.jsxElement = { }

def ProofWidgets.Jsx.jsxElement.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.jsxChild : Lean.Parser.Category

Equations

• Lean.Parser.Category.jsxChild = { }

def ProofWidgets.Jsx.jsxChild.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.jsxAttr : Lean.Parser.Category

Equations

• Lean.Parser.Category.jsxAttr = { }

def ProofWidgets.Jsx.jsxAttr.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.jsxAttrVal : Lean.Parser.Category

Equations

• Lean.Parser.Category.jsxAttrVal = { }

def ProofWidgets.Jsx.jsxAttrVal.quot : Lean.ParserDescr

Equations

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

def ProofWidgets.Jsx.jsxAttrVal_ : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.jsxAttrVal_ = Lean.ParserDescr.node `ProofWidgets.Jsx.jsxAttrVal_ 1022 (Lean.ParserDescr.const `str)

def ProofWidgets.Jsx.«jsxAttrVal{_}» : Lean.ParserDescr

Equations

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

def ProofWidgets.Jsx.«jsxAttr_=_» : Lean.ParserDescr

Equations

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

def ProofWidgets.Jsx.jsxText : Lean.Parser.Parser

Equations

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

def ProofWidgets.Jsx.getJsxText : Lean.TSyntax `jsxText → String

Equations

• ProofWidgets.Jsx.getJsxText x = let stx := x; Lean.Syntax.getAtomVal stx.raw[0]

def ProofWidgets.Jsx.jsxText.formatter : Lean.PrettyPrinter.Formatter

Equations

• ProofWidgets.Jsx.jsxText.formatter = Lean.PrettyPrinter.Formatter.visitAtom `jsxText

def ProofWidgets.Jsx.jsxText.parenthesizer : Lean.PrettyPrinter.Parenthesizer

Equations

• ProofWidgets.Jsx.jsxText.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

def ProofWidgets.Jsx.«jsxElement<__/>» : Lean.ParserDescr

Equations

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

def ProofWidgets.Jsx.«jsxElement<__>_» : Lean.ParserDescr

Equations

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

def ProofWidgets.Jsx.jsxChild_ : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.jsxChild_ = Lean.ParserDescr.node `ProofWidgets.Jsx.jsxChild_ 1022 (Lean.ParserDescr.parser `ProofWidgets.Jsx.jsxText)

def ProofWidgets.Jsx.«jsxChild{_}» : Lean.ParserDescr

Equations

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

def ProofWidgets.Jsx.jsxChild__1 : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.jsxChild__1 = Lean.ParserDescr.node `ProofWidgets.Jsx.jsxChild__1 1022 (Lean.ParserDescr.cat `jsxElement 0)

def ProofWidgets.Jsx.term_ : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.term_ = Lean.ParserDescr.node `ProofWidgets.Jsx.term_ 1024 (Lean.ParserDescr.cat `jsxElement 0)

def ProofWidgets.Jsx.transformTag (n : Lean.Ident) (m : Lean.Ident) (ns : Array Lean.Ident) (vs : Array (Lean.TSyntax `jsxAttrVal)) (cs : Array (Lean.TSyntax `jsxChild)) : Lean.MacroM Lean.Term

Equations

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

def ProofWidgets.Jsx.delabJsxChildren : Lean.PrettyPrinter.Delaborator.DelabM (Array (Lean.TSyntax `jsxChild))

Equations

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

def ProofWidgets.Jsx.delabHtmlElement : Lean.PrettyPrinter.Delaborator.Delab

Equations

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

def ProofWidgets.Jsx.delabHtmlOfComponent : Lean.PrettyPrinter.Delaborator.Delab

Equations

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