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 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 ProofWidgets.instInhabitedHtml : Inhabited Html

instance ProofWidgets.instRpcEncodableHtml : Lean.Server.RpcEncodable Html

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

inductive ProofWidgets.LayoutKind : Type

See MDN docs.

• block : LayoutKind
• inline : LayoutKind

def Lean.Parser.Category.jsxElement : Category

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

def Lean.Parser.Category.jsxChild : Category

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

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

def Lean.Parser.Category.jsxAttr : Category

def Lean.Parser.Category.jsxAttrVal : Category

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

def ProofWidgets.Jsx.jsxAttrVal_ : Lean.ParserDescr

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

Interpolates an expression into a JSX attribute literal.

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

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

Interpolates a collection into a JSX attribute literal. For HTML tags, this should have type Array (String × Json). For ProofWidgets.Components, it can be any structure $t whatsoever: it is interpolated into the component's props using { $t with ... } notation.

def ProofWidgets.Jsx.jsxTextForbidden : String

Characters not allowed inside JSX plain text.

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

A plain text literal for JSX (notation for Html.text).

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

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

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

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

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

def ProofWidgets.Jsx.jsxChild_ : Lean.ParserDescr

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

Interpolates an array of elements into a JSX literal

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

Interpolates an expression into a JSX literal

def ProofWidgets.Jsx.jsxChild__1 : Lean.ParserDescr

def ProofWidgets.Jsx.term_ : Lean.ParserDescr

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

First delaborate into our non-term TSyntax. Note this means we can't call delab, so we have to add the term annotations ourselves.

def ProofWidgets.Jsx.delabHtmlText : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `ProofWidgets.Jsx.jsxText)

partial def ProofWidgets.Jsx.delabHtmlElement' : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `jsxElement)

partial def ProofWidgets.Jsx.delabHtmlOfComponent' : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `jsxElement)

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

Now wrap our TSyntax _ delaborators into Term elaborators.

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

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