Parsers for HTML syntax

• Compliant with the HTML living standard to the extent that it makes sense. Departures are documented on the appropriate parsers.

• We eschew Lean's standard mechanism of syntactic categories in favor of hand-rolled parsers, formatters, and parenthesizers for two reasons:

  • Lean parsers generally consume trailing whitespace, whereas certain HTML parsers (e.g. end tag > symbols) should not do so, so that this whitespace is instead included in text content following those parsers.

  • Category parsing inspects the leading token and dispatches to the appropriate parser whereas we allow text contents to begin with reserved symbols such as '.

• In content, all whitespace is preserved by parsers, and then collapsed in Content.view.

• To simplify away special handling of $, most parsers here cannot be antiquoted. Parsers that can be antiquoted are documented as such.

• The docstrings of certain parsers are shown in IDEs on hover. These parsers may contain additional, non-docstring comments describing non-user-facing implementation details.

Helpers

Character references

def Lean.Html.Syntax.decodeCharacterReferenceAt (s : String) (i : String.Pos.Raw) (refAt : String.Pos.Raw → String.Pos.Raw → Syntax) : CoreM (String × String.Pos.Raw)

Decodes one character reference starting at i, which must point at at the character & in s. Returns the decoded string, and the position just after ;.

Errors are reported at refAt, which should produce the subsyntax between two offsets into s.

Equations

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

def Lean.Html.Syntax.decodeCharacterReferences (ref : TSyntax `str) : CoreM String

Decodes HTML character references in ref, leaving other characters unchanged.

Equations

• Lean.Html.Syntax.decodeCharacterReferences ref = Lean.Html.Syntax.decodeCharacterReferences.go✝ ref ref.getString { } ""

Raw symbols

def Lean.Html.Syntax.rawSymbol (sym : String) (trailingWs : Bool := false) (expected : List String := [toString "'" ++ toString sym ++ toString "'"]) : Parser.Parser

Parses sym as an atom. Unlike symbol, this parser does not consult the token table, and sym is not registered as a token.

Trailing whitespace (including Lean-style comments) is consumed and stored in the atom only if trailingWs is set; otherwise it is left to the next parser.

Equations

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

def Lean.Html.Syntax.rawSymbol.parenthesizer (sym : String) : Bool → List String → PrettyPrinter.ParenthesizerM Unit

Equations

• Lean.Html.Syntax.rawSymbol.parenthesizer sym x✝¹ x✝ = Lean.PrettyPrinter.Parenthesizer.symbolNoAntiquot.parenthesizer sym

def Lean.Html.Syntax.rawSymbol.formatter (sym : String) : Bool → List String → PrettyPrinter.Formatter

Equations

• Lean.Html.Syntax.rawSymbol.formatter sym x✝¹ x✝ = do Lean.PrettyPrinter.Formatter.resetLeadWord Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter sym

Interpolations

def Lean.Html.Syntax.interpWith (kind : SyntaxNodeKind) (openSym : String) (trailingWs : Bool) : Parser.Parser

Parses an interpolation: a Lean term between openSym and }. Trailing whitespace is consumed only if trailingWs is set.

Equations

• Lean.Html.Syntax.interpWith kind openSym trailingWs = Lean.Parser.node kind (Lean.Html.Syntax.rawSymbol openSym true >> Lean.Parser.termParser >> Lean.Html.Syntax.rawSymbol "}" trailingWs)

def Lean.Html.Syntax.interp (trailingWs : Bool := false) : Parser.Parser

Equations

• Lean.Html.Syntax.interp trailingWs = Lean.Html.Syntax.interpWith `Lean.Html.Syntax.interp "{" trailingWs

def Lean.Html.Syntax.interpMany (trailingWs : Bool := false) : Parser.Parser

Equations

• Lean.Html.Syntax.interpMany trailingWs = Lean.Html.Syntax.interpWith `Lean.Html.Syntax.interpMany "{..." trailingWs

@[reducible, inline]

abbrev Lean.Html.Syntax.interpKind (isMany : Bool) : Name

Equations

• Lean.Html.Syntax.interpKind isMany = if isMany = true then `Lean.Html.Syntax.interpMany else `Lean.Html.Syntax.interp

@[reducible, inline]

abbrev Lean.Html.Syntax.Interp (isMany : Bool) : Type

Equations

• Lean.Html.Syntax.Interp isMany = Lean.TSyntax (Lean.Html.Syntax.interpKind isMany)

structure Lean.Html.Syntax.InterpView (isMany : Bool) : Type

A single-element { term } or many-element {... term } interpolation.

• openBrace : Syntax

  { or {....

• term : Term

  The interpolated term.

• closeBrace : Syntax

  }.

@[instance_reducible]

instance Lean.Html.Syntax.instReprInterpView {isMany✝ : Bool} : Repr (InterpView isMany✝)

Equations

• Lean.Html.Syntax.instReprInterpView = { reprPrec := Lean.Html.Syntax.instReprInterpView.repr }

def Lean.Html.Syntax.instReprInterpView.repr {isMany✝ : Bool} : InterpView isMany✝ → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedInterpView {a✝ : Bool} : Inhabited (InterpView a✝)

Equations

• Lean.Html.Syntax.instInhabitedInterpView = { default := Lean.Html.Syntax.instInhabitedInterpView.default }

@[instance_reducible]

instance Lean.Html.Syntax.instBEqInterpView {isMany✝ : Bool} : BEq (InterpView isMany✝)

Equations

• Lean.Html.Syntax.instBEqInterpView = { beq := Lean.Html.Syntax.instBEqInterpView.beq }

def Lean.Html.Syntax.instBEqInterpView.beq {isMany✝ : Bool} : InterpView isMany✝ → InterpView isMany✝ → Bool

Equations

• Lean.Html.Syntax.instBEqInterpView.beq { openBrace := a, term := a_1, closeBrace := a_2 } { openBrace := b, term := b_1, closeBrace := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Html.Syntax.instBEqInterpView.beq x✝¹ x✝ = false

def Lean.Html.Syntax.Interp.view {m : Type → Type} {isMany : Bool} [Monad m] [MonadError m] (stx : Interp isMany) : m (InterpView isMany)

Equations

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

def Lean.Html.Syntax.InterpView.of {m : Type → Type} {isMany : Bool} [Monad m] [MonadError m] (stx : Interp isMany) : m (InterpView isMany)

Equations

• @Lean.Html.Syntax.InterpView.of = @Lean.Html.Syntax.Interp.view

Text content

def Lean.Html.Syntax.text : Parser.Parser

HTML text content.

Equations

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

@[reducible, inline]

abbrev Lean.Html.Syntax.textKind : Name

Equations

• Lean.Html.Syntax.textKind = `Lean.Html.Syntax.text

@[reducible, inline]

abbrev Lean.Html.Syntax.Text : Type

Equations

• Lean.Html.Syntax.Text = Lean.TSyntax Lean.Html.Syntax.textKind

def Lean.Html.Syntax.text.parenthesizer : PrettyPrinter.Parenthesizer

Equations

• Lean.Html.Syntax.text.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lean.Html.Syntax.text.formatter : PrettyPrinter.Formatter

Equations

• Lean.Html.Syntax.text.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.Html.Syntax.textKind

Comments

def Lean.Html.Syntax.comment : Parser.Parser

An HTML comment.

Equations

• Lean.Html.Syntax.comment = { info := Lean.Parser.nodeInfo `Lean.Html.Syntax.comment { }, fn := Lean.Parser.nodeFn `Lean.Html.Syntax.comment (Lean.Parser.rawFn Lean.Html.Syntax.commentFn✝) }

@[reducible, inline]

abbrev Lean.Html.Syntax.commentKind : Name

Equations

• Lean.Html.Syntax.commentKind = `Lean.Html.Syntax.comment

@[reducible, inline]

abbrev Lean.Html.Syntax.Comment : Type

Equations

• Lean.Html.Syntax.Comment = Lean.TSyntax Lean.Html.Syntax.commentKind

def Lean.Html.Syntax.comment.parenthesizer : PrettyPrinter.Parenthesizer

Equations

• Lean.Html.Syntax.comment.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lean.Html.Syntax.comment.formatter : PrettyPrinter.Formatter

Equations

• Lean.Html.Syntax.comment.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.Html.Syntax.commentKind

def Lean.Html.Syntax.Comment.view {m : Type → Type} [Monad m] [MonadError m] : Comment → m String

Text contents of an HTML comment, excluding start and end markers.

Equations

• x✝.view = match x✝ with | { raw := Lean.Syntax.node info kind #[Lean.Syntax.atom info_1 s] } => pure ((s.drop 4).dropEnd 3).toString | x => Lean.Elab.throwUnsupportedSyntax

Tag names

def Lean.Html.Syntax.tagName : Parser.Parser

An HTML tag name: an ASCII letter followed by characters other than ASCII whitespace, U+0000 NULL, /, >. This includes custom element names.

Equations

• Lean.Html.Syntax.tagName = Lean.Html.Syntax.parseFirstMany✝ `Lean.Html.Syntax.tagName "tag name" Char.isAlpha Lean.Html.Syntax.tagName.isTagNameChar✝

@[reducible, inline]

abbrev Lean.Html.Syntax.tagNameKind : Name

Equations

• Lean.Html.Syntax.tagNameKind = `Lean.Html.Syntax.tagName

@[reducible, inline]

abbrev Lean.Html.Syntax.TagName : Type

Equations

• Lean.Html.Syntax.TagName = Lean.TSyntax Lean.Html.Syntax.tagNameKind

def Lean.Html.Syntax.TagName.view {m : Type → Type} [Monad m] [MonadError m] : TagName → m String

Equations

• Lean.Html.Syntax.TagName.view = Lean.Html.Syntax.viewNodeAtom✝

Attribute names

def Lean.Html.Syntax.attrName : Parser.Parser

An HTML attribute name. Attribute names may not start with { (which would conflict with interpolation).

Equations

• Lean.Html.Syntax.attrName = Lean.Html.Syntax.parseFirstMany✝ `Lean.Html.Syntax.attrName "attribute name" Lean.Html.Syntax.attrName.isAttrNameFirstChar✝ Lean.Html.Syntax.attrName.isAttrNameChar✝

@[reducible, inline]

abbrev Lean.Html.Syntax.attrNameKind : Name

Equations

• Lean.Html.Syntax.attrNameKind = `Lean.Html.Syntax.attrName

@[reducible, inline]

abbrev Lean.Html.Syntax.AttrName : Type

Equations

• Lean.Html.Syntax.AttrName = Lean.TSyntax Lean.Html.Syntax.attrNameKind

def Lean.Html.Syntax.AttrName.view {m : Type → Type} [Monad m] [MonadError m] : AttrName → m String

Equations

• Lean.Html.Syntax.AttrName.view = Lean.Html.Syntax.viewNodeAtom✝

Attribute values

def Lean.Html.Syntax.attrVal : Parser.Parser

Equations

• Lean.Html.Syntax.attrVal = Lean.Parser.node `Lean.Html.Syntax.attrVal (Lean.Parser.strLit <|> Lean.Html.Syntax.interp true)

@[reducible, inline]

abbrev Lean.Html.Syntax.attrValKind : Name

Equations

• Lean.Html.Syntax.attrValKind = `Lean.Html.Syntax.attrVal

@[reducible, inline]

abbrev Lean.Html.Syntax.AttrVal : Type

Equations

• Lean.Html.Syntax.AttrVal = Lean.TSyntax Lean.Html.Syntax.attrValKind

inductive Lean.Html.Syntax.AttrValView : Type

• str (stx : TSyntax `str) : AttrValView

  A string literal. Character references in the literal must be decoded before use (via decodeCharacterReferences).

• interp (stx : Interp false) : AttrValView

def Lean.Html.Syntax.instReprAttrValView.repr : AttrValView → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprAttrValView : Repr AttrValView

Equations

• Lean.Html.Syntax.instReprAttrValView = { reprPrec := Lean.Html.Syntax.instReprAttrValView.repr }

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedAttrValView : Inhabited AttrValView

Equations

• Lean.Html.Syntax.instInhabitedAttrValView = { default := Lean.Html.Syntax.instInhabitedAttrValView.default }

def Lean.Html.Syntax.instBEqAttrValView.beq : AttrValView → AttrValView → Bool

Equations

• Lean.Html.Syntax.instBEqAttrValView.beq (Lean.Html.Syntax.AttrValView.str a) (Lean.Html.Syntax.AttrValView.str b) = (a == b)
• Lean.Html.Syntax.instBEqAttrValView.beq (Lean.Html.Syntax.AttrValView.interp a) (Lean.Html.Syntax.AttrValView.interp b) = (a == b)
• Lean.Html.Syntax.instBEqAttrValView.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Html.Syntax.instBEqAttrValView : BEq AttrValView

Equations

• Lean.Html.Syntax.instBEqAttrValView = { beq := Lean.Html.Syntax.instBEqAttrValView.beq }

def Lean.Html.Syntax.AttrVal.view {m : Type → Type} [Monad m] [MonadError m] (stx : AttrVal) : m AttrValView

Provides a view on the attribute value, decoding character references when the value is a string literal.

Equations

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

def Lean.Html.Syntax.AttrValView.of {m : Type → Type} [Monad m] [MonadError m] (stx : AttrVal) : m AttrValView

Equations

• @Lean.Html.Syntax.AttrValView.of = @Lean.Html.Syntax.AttrVal.view

Attributes

def Lean.Html.Syntax.attr : Parser.Parser

An HTML attribute. We support double-quoted attribute values <tag name="val">, empty attributes <tag name>, interpolations of one value <tag name={ term }>, and interpolations of a sequence of attributes <tag {... term }/>. Character references are decoded in double-quoted values.

Equations

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

@[reducible, inline]

abbrev Lean.Html.Syntax.attrKind : Name

Equations

• Lean.Html.Syntax.attrKind = `Lean.Html.Syntax.attr

@[reducible, inline]

abbrev Lean.Html.Syntax.Attr : Type

Equations

• Lean.Html.Syntax.Attr = Lean.TSyntax Lean.Html.Syntax.attrKind

structure Lean.Html.Syntax.ValAttrView : Type

• name : AttrName
• eq : Syntax

  The = symbol.

• val : AttrVal

def Lean.Html.Syntax.instReprValAttrView.repr : ValAttrView → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprValAttrView : Repr ValAttrView

Equations

• Lean.Html.Syntax.instReprValAttrView = { reprPrec := Lean.Html.Syntax.instReprValAttrView.repr }

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedValAttrView : Inhabited ValAttrView

Equations

• Lean.Html.Syntax.instInhabitedValAttrView = { default := Lean.Html.Syntax.instInhabitedValAttrView.default }

@[instance_reducible]

instance Lean.Html.Syntax.instBEqValAttrView : BEq ValAttrView

Equations

• Lean.Html.Syntax.instBEqValAttrView = { beq := Lean.Html.Syntax.instBEqValAttrView.beq }

def Lean.Html.Syntax.instBEqValAttrView.beq : ValAttrView → ValAttrView → Bool

Equations

• Lean.Html.Syntax.instBEqValAttrView.beq { name := a, eq := a_1, val := a_2 } { name := b, eq := b_1, val := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Html.Syntax.instBEqValAttrView.beq x✝¹ x✝ = false

inductive Lean.Html.Syntax.AttrView : Type

• val (stx : ValAttrView) : AttrView
• bool (stx : AttrName) : AttrView
• interp (isMany : Bool) (stx : Interp isMany) : AttrView

@[instance_reducible]

instance Lean.Html.Syntax.instReprAttrView : Repr AttrView

Equations

• Lean.Html.Syntax.instReprAttrView = { reprPrec := Lean.Html.Syntax.instReprAttrView.repr }

def Lean.Html.Syntax.instReprAttrView.repr : AttrView → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedAttrView : Inhabited AttrView

Equations

• Lean.Html.Syntax.instInhabitedAttrView = { default := Lean.Html.Syntax.instInhabitedAttrView.default }

@[instance_reducible]

instance Lean.Html.Syntax.instBEqAttrView : BEq AttrView

Equations

• Lean.Html.Syntax.instBEqAttrView = { beq := Lean.Html.Syntax.instBEqAttrView.beq }

def Lean.Html.Syntax.instBEqAttrView.beq : AttrView → AttrView → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Html.Syntax.instBEqAttrView.beq (Lean.Html.Syntax.AttrView.val a) (Lean.Html.Syntax.AttrView.val b) = (a == b)
• Lean.Html.Syntax.instBEqAttrView.beq (Lean.Html.Syntax.AttrView.bool a) (Lean.Html.Syntax.AttrView.bool b) = (a == b)
• Lean.Html.Syntax.instBEqAttrView.beq x✝¹ x✝ = false

def Lean.Html.Syntax.Attr.view {m : Type → Type} [Monad m] [MonadError m] (stx : Attr) : m AttrView

Equations

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

def Lean.Html.Syntax.AttrView.of {m : Type → Type} [Monad m] [MonadError m] (stx : Attr) : m AttrView

Equations

• @Lean.Html.Syntax.AttrView.of = @Lean.Html.Syntax.Attr.view

Elements and content

Content is not a syntax category because a category parser starts by reading a Lean token, which fails on text that begins with whitespace or, for example, '. Instead, contentItemFn dispatches to item parsers based on the next character.

@[reducible, inline]

abbrev Lean.Html.Syntax.elementKind : Name

Equations

• Lean.Html.Syntax.elementKind = `Lean.Html.Syntax.element

@[reducible, inline]

abbrev Lean.Html.Syntax.Element : Type

Equations

• Lean.Html.Syntax.Element = Lean.TSyntax Lean.Html.Syntax.elementKind

@[reducible, inline]

abbrev Lean.Html.Syntax.contentKind : Name

Equations

• Lean.Html.Syntax.contentKind = `Lean.Html.Syntax.content

@[reducible, inline]

abbrev Lean.Html.Syntax.Content : Type

A sequence of HTML text nodes, comments, elements, and interpolations.

Equations

• Lean.Html.Syntax.Content = Lean.TSyntax Lean.Html.Syntax.contentKind

def Lean.Html.Syntax.elementWith (content : Parser.Parser) : Parser.Parser

Equations

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

structure Lean.Html.Syntax.TagView : Type

• lt : Syntax

  < or </.

• name : TagName
• attrs : Array Attr

  Attributes on the tag. Always empty in end tags.

• gt : Syntax

  > or />.

@[instance_reducible]

instance Lean.Html.Syntax.instReprTagView : Repr TagView

Equations

• Lean.Html.Syntax.instReprTagView = { reprPrec := Lean.Html.Syntax.instReprTagView.repr }

def Lean.Html.Syntax.instReprTagView.repr : TagView → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedTagView : Inhabited TagView

Equations

• Lean.Html.Syntax.instInhabitedTagView = { default := Lean.Html.Syntax.instInhabitedTagView.default }

def Lean.Html.Syntax.instBEqTagView.beq : TagView → TagView → Bool

Equations

• Lean.Html.Syntax.instBEqTagView.beq { lt := a, name := a_1, attrs := a_2, gt := a_3 } { lt := b, name := b_1, attrs := b_2, gt := b_3 } = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• Lean.Html.Syntax.instBEqTagView.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Html.Syntax.instBEqTagView : BEq TagView

Equations

• Lean.Html.Syntax.instBEqTagView = { beq := Lean.Html.Syntax.instBEqTagView.beq }

structure Lean.Html.Syntax.ElementView : Type

• startTag : TagView
• children? : Option Content

  HTML content between the start and end tags.

• endTag? : Option TagView

  The end tag, if the element is not self-closing.

@[instance_reducible]

instance Lean.Html.Syntax.instReprElementView : Repr ElementView

Equations

• Lean.Html.Syntax.instReprElementView = { reprPrec := Lean.Html.Syntax.instReprElementView.repr }

def Lean.Html.Syntax.instReprElementView.repr : ElementView → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedElementView : Inhabited ElementView

Equations

• Lean.Html.Syntax.instInhabitedElementView = { default := Lean.Html.Syntax.instInhabitedElementView.default }

@[instance_reducible]

instance Lean.Html.Syntax.instBEqElementView : BEq ElementView

Equations

• Lean.Html.Syntax.instBEqElementView = { beq := Lean.Html.Syntax.instBEqElementView.beq }

def Lean.Html.Syntax.instBEqElementView.beq : ElementView → ElementView → Bool

Equations

• Lean.Html.Syntax.instBEqElementView.beq { startTag := a, children? := a_1, endTag? := a_2 } { startTag := b, children? := b_1, endTag? := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Html.Syntax.instBEqElementView.beq x✝¹ x✝ = false

def Lean.Html.Syntax.Element.view {m : Type → Type} [Monad m] [MonadError m] (stx : Element) : m ElementView

Equations

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

def Lean.Html.Syntax.ElementView.of {m : Type → Type} [Monad m] [MonadError m] (stx : Element) : m ElementView

Equations

• @Lean.Html.Syntax.ElementView.of = @Lean.Html.Syntax.Element.view

def Lean.Html.Syntax.contentWith (itemFn : Parser.ParserFn) : Parser.Parser

Equations

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

def Lean.Html.Syntax.content : Parser.Parser

A sequence of HTML content nodes: text contents, comments, elements, single-item interpolations { term }, and many-item interpolations {... term } (see interpMany).

Equations

• Lean.Html.Syntax.content = Lean.Html.Syntax.contentWith Lean.Html.Syntax.contentItemFn✝

partial def Lean.Html.Syntax.content.parenthesizer : PrettyPrinter.Parenthesizer

partial def Lean.Html.Syntax.contentItem.parenthesizer : PrettyPrinter.Parenthesizer

partial def Lean.Html.Syntax.content.formatter : PrettyPrinter.Formatter

partial def Lean.Html.Syntax.contentItem.formatter : PrettyPrinter.Formatter

def Lean.Html.Syntax.element : Parser.Parser

An HTML element: <tag attr*/> or <tag attr*>content</tag>.

Tags must be closed: void element syntax such as <br>, and implied end tags such as <ul><li>item</ul>, are not supported.

Equations

• Lean.Html.Syntax.element = Lean.Html.Syntax.elementWith Lean.Html.Syntax.content

structure Lean.Html.Syntax.TextCommentsView : Type

Consecutive run of text nodes and comments.

• stxs : Array (Text ⊕ Comment)

def Lean.Html.Syntax.instReprTextCommentsView.repr : TextCommentsView → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprTextCommentsView : Repr TextCommentsView

Equations

• Lean.Html.Syntax.instReprTextCommentsView = { reprPrec := Lean.Html.Syntax.instReprTextCommentsView.repr }

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedTextCommentsView : Inhabited TextCommentsView

Equations

• Lean.Html.Syntax.instInhabitedTextCommentsView = { default := Lean.Html.Syntax.instInhabitedTextCommentsView.default }

def Lean.Html.Syntax.instBEqTextCommentsView.beq : TextCommentsView → TextCommentsView → Bool

Equations

• Lean.Html.Syntax.instBEqTextCommentsView.beq { stxs := a } { stxs := b } = (a == b)
• Lean.Html.Syntax.instBEqTextCommentsView.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Html.Syntax.instBEqTextCommentsView : BEq TextCommentsView

Equations

• Lean.Html.Syntax.instBEqTextCommentsView = { beq := Lean.Html.Syntax.instBEqTextCommentsView.beq }

def Lean.Html.Syntax.TextCommentsView.getText (v : TextCommentsView) : CoreM String

Returns the normalized text contents of this sequence of text nodes and comments:

• Whitespace that contains a newline (U+000A or U+000D), and is not surrounded by text on both sides, is removed.

• Other consecutive whitespace is collapsed into a single space (U+0020).

• HTML character references are decoded into the Unicode characters they represent.

Throws if an invalid character reference is encountered in the text.

Equations

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

def Lean.Html.Syntax.TextCommentsView.getSyntax (v : TextCommentsView) : Syntax

A syntax spanning all nodes in this view. Useful for reporting elaboration errors.

Equations

• v.getSyntax = Lean.mkNullNode (Array.map (Sum.elim Lean.TSyntax.raw Lean.TSyntax.raw) v.stxs)

inductive Lean.Html.Syntax.ContentItemView : Type

• element (stx : Element) : ContentItemView
• textComments (stx : TextCommentsView) : ContentItemView
• interp (isMany : Bool) (stx : Interp isMany) : ContentItemView

def Lean.Html.Syntax.instReprContentItemView.repr : ContentItemView → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprContentItemView : Repr ContentItemView

Equations

• Lean.Html.Syntax.instReprContentItemView = { reprPrec := Lean.Html.Syntax.instReprContentItemView.repr }

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedContentItemView : Inhabited ContentItemView

Equations

• Lean.Html.Syntax.instInhabitedContentItemView = { default := Lean.Html.Syntax.instInhabitedContentItemView.default }

def Lean.Html.Syntax.instBEqContentItemView.beq : ContentItemView → ContentItemView → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Html.Syntax.instBEqContentItemView.beq (Lean.Html.Syntax.ContentItemView.element a) (Lean.Html.Syntax.ContentItemView.element b) = (a == b)
• Lean.Html.Syntax.instBEqContentItemView.beq (Lean.Html.Syntax.ContentItemView.textComments a) (Lean.Html.Syntax.ContentItemView.textComments b) = (a == b)
• Lean.Html.Syntax.instBEqContentItemView.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Html.Syntax.instBEqContentItemView : BEq ContentItemView

Equations

• Lean.Html.Syntax.instBEqContentItemView = { beq := Lean.Html.Syntax.instBEqContentItemView.beq }

def Lean.Html.Syntax.Content.view {m : Type → Type} [Monad m] [MonadError m] (c : Content) : m (Array ContentItemView)

Returns the sequence of items in an HTML content node.

Runs of text interspersed with comments are merged into a single item. This is because their text must be processed together into a single output (see TextCommentsView.getText).

Equations

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

def Lean.Html.Syntax.«html%» : Parser.Parser

An HTML literal.

Equations

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