This module defines:

• a representation of HTML trees
• together with a JSX-like DSL for writing them
• and widget support for visualizing any type as HTML.

inductive DocGen4.Html : Type

• element : String → Bool → Array (String × String) → Array Html → Html
• text : String → Html

  A text node, which will be escaped in the output

• raw : String → Html

  An arbitrary string containing HTML

partial def DocGen4.instReprHtml.repr : Html → Nat → Std.Format

@[implicit_reducible]

instance DocGen4.instReprHtml : Repr Html

Equations

• DocGen4.instReprHtml = { reprPrec := DocGen4.instReprHtml.repr }

@[implicit_reducible]

instance DocGen4.instBEqHtml : BEq Html

Equations

• DocGen4.instBEqHtml = { beq := DocGen4.instBEqHtml.beq }

partial def DocGen4.instBEqHtml.beq : Html → Html → Bool

@[implicit_reducible]

instance DocGen4.instInhabitedHtml : Inhabited Html

Equations

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

@[implicit_reducible]

instance DocGen4.instFromJsonHtml : Lean.FromJson Html

Equations

• DocGen4.instFromJsonHtml = { fromJson? := DocGen4.instFromJsonHtml.fromJson }

partial def DocGen4.instFromJsonHtml.fromJson : Lean.Json → Except String Html

partial def DocGen4.instToJsonHtml.toJson : Html → Lean.Json

@[implicit_reducible]

instance DocGen4.instToJsonHtml : Lean.ToJson Html

Equations

• DocGen4.instToJsonHtml = { toJson := DocGen4.instToJsonHtml.toJson }

@[implicit_reducible]

instance DocGen4.instCoeStringHtml : Coe String Html

Equations

• DocGen4.instCoeStringHtml = { coe := DocGen4.Html.text }

def DocGen4.Html.escape (s : String) : String

Equations

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

def DocGen4.Html.escape.subst : Char → Option String

Equations

• DocGen4.Html.escape.subst '&' = some "&"
• DocGen4.Html.escape.subst '<' = some "&lt;"
• DocGen4.Html.escape.subst '>' = some "&gt;"
• DocGen4.Html.escape.subst '\"' = some "&quot;"
• DocGen4.Html.escape.subst a✝ = none

def DocGen4.Html.attributesToString (attrs : Array (String × String)) : String

Equations

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

partial def DocGen4.Html.toStringAux : Html → String

def DocGen4.Html.toString (html : Html) : String

Equations

• html.toString = html.toStringAux.trimAsciiEnd.copy

partial def DocGen4.Html.textLength : Html → Nat

def Lean.Parser.Category.jsxElement : Category

Equations

• Lean.Parser.Category.jsxElement = { }

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

Equations

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

def Lean.Parser.Category.jsxChild : Category

Equations

• Lean.Parser.Category.jsxChild = { }

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

Equations

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

def DocGen4.Jsx.jsxText : Lean.Parser.Parser

Equations

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

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

Equations

• DocGen4.Jsx.jsxText.formatter = pure ()

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

Equations

• DocGen4.Jsx.jsxText.parenthesizer = pure ()

def DocGen4.Jsx.jsxAttrName : Lean.ParserDescr

Equations

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

def DocGen4.Jsx.jsxAttrVal : Lean.ParserDescr

Equations

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

def DocGen4.Jsx.jsxSimpleAttr : Lean.ParserDescr

Equations

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

def DocGen4.Jsx.jsxAttrSpread : Lean.ParserDescr

Equations

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

def DocGen4.Jsx.jsxAttr : Lean.ParserDescr

Equations

• DocGen4.Jsx.jsxAttr = Lean.ParserDescr.nodeWithAntiquot "jsxAttr" `DocGen4.Jsx.jsxAttr (Lean.ParserDescr.binary `orelse DocGen4.Jsx.jsxSimpleAttr DocGen4.Jsx.jsxAttrSpread)

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

Equations

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

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

Equations

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

def DocGen4.Jsx.jsxChild_ : Lean.ParserDescr

Equations

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

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

Equations

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

def DocGen4.Jsx.«jsxChild[_]» : Lean.ParserDescr

Equations

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

def DocGen4.Jsx.jsxChild__1 : Lean.ParserDescr

Equations

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

def DocGen4.Jsx.term_ : Lean.ParserDescr

Equations

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

def DocGen4.Jsx.translateAttrs (attrs : Array (Lean.TSyntax `DocGen4.Jsx.jsxAttr)) : Lean.MacroM (Lean.TSyntax `term)

Equations

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

class DocGen4.ToHtmlFormat (α : Type u) : Type u

A type which implements ToHtmlFormat will be visualized as the resulting HTML in editors which support it.

• formatHtml : α → Html