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.

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

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

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.

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

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

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.

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

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

@[reducible, inline]

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

@[reducible, inline]

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

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✝)

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

@[instance_reducible]

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

@[instance_reducible]

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

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

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

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

Text content

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

HTML text content.

@[reducible, inline]

abbrev Lean.Html.Syntax.textKind : Name

@[reducible, inline]

abbrev Lean.Html.Syntax.Text : Type

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

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

Comments

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

An HTML comment.

@[reducible, inline]

abbrev Lean.Html.Syntax.commentKind : Name

@[reducible, inline]

abbrev Lean.Html.Syntax.Comment : Type

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

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

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.

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.

@[reducible, inline]

abbrev Lean.Html.Syntax.tagNameKind : Name

@[reducible, inline]

abbrev Lean.Html.Syntax.TagName : Type

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

Attribute names

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

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

@[reducible, inline]

abbrev Lean.Html.Syntax.attrNameKind : Name

@[reducible, inline]

abbrev Lean.Html.Syntax.AttrName : Type

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

Attribute values

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

@[reducible, inline]

abbrev Lean.Html.Syntax.attrValKind : Name

@[reducible, inline]

abbrev Lean.Html.Syntax.AttrVal : Type

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprAttrValView : Repr AttrValView

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedAttrValView : Inhabited AttrValView

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

@[instance_reducible]

instance Lean.Html.Syntax.instBEqAttrValView : BEq AttrValView

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.

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

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.

@[reducible, inline]

abbrev Lean.Html.Syntax.attrKind : Name

@[reducible, inline]

abbrev Lean.Html.Syntax.Attr : Type

structure Lean.Html.Syntax.ValAttrView : Type

• name : AttrName
• eq : Syntax

  The = symbol.

• val : AttrVal

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprValAttrView : Repr ValAttrView

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedValAttrView : Inhabited ValAttrView

@[instance_reducible]

instance Lean.Html.Syntax.instBEqValAttrView : BEq ValAttrView

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

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

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

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedAttrView : Inhabited AttrView

@[instance_reducible]

instance Lean.Html.Syntax.instBEqAttrView : BEq AttrView

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

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

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

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

@[reducible, inline]

abbrev Lean.Html.Syntax.Element : Type

@[reducible, inline]

abbrev Lean.Html.Syntax.contentKind : Name

@[reducible, inline]

abbrev Lean.Html.Syntax.Content : Type

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

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

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

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

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedTagView : Inhabited TagView

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

@[instance_reducible]

instance Lean.Html.Syntax.instBEqTagView : BEq TagView

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

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

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedElementView : Inhabited ElementView

@[instance_reducible]

instance Lean.Html.Syntax.instBEqElementView : BEq ElementView

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

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

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

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

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).

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.

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprTextCommentsView : Repr TextCommentsView

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedTextCommentsView : Inhabited TextCommentsView

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

@[instance_reducible]

instance Lean.Html.Syntax.instBEqTextCommentsView : BEq TextCommentsView

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.

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

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

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

@[instance_reducible]

instance Lean.Html.Syntax.instReprContentItemView : Repr ContentItemView

@[instance_reducible]

instance Lean.Html.Syntax.instInhabitedContentItemView : Inhabited ContentItemView

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

@[instance_reducible]

instance Lean.Html.Syntax.instBEqContentItemView : BEq ContentItemView

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).

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

An HTML literal.