def Lean.Doc.Parser.skipFn : Parser.ParserFn

A parser that does nothing.

Equations

• Lean.Doc.Parser.skipFn x✝ s = s

def Lean.Doc.Parser.isRefNameChar : Char → Bool

Whether c may appear in the name of a footnote or a link reference. A name is written literally, so a backslash denotes itself elsewhere and is not part of a name.

Equations

• Lean.Doc.Parser.isRefNameChar '[' = false
• Lean.Doc.Parser.isRefNameChar ']' = false
• Lean.Doc.Parser.isRefNameChar '^' = false
• Lean.Doc.Parser.isRefNameChar '\\' = false
• Lean.Doc.Parser.isRefNameChar '\n' = false
• Lean.Doc.Parser.isRefNameChar '\t' = false
• Lean.Doc.Parser.isRefNameChar x✝ = true

def Lean.Doc.Parser.ignoreFn (p : Parser.ParserFn) : Parser.ParserFn

Parses as p, but discards the result.

Equations

• Lean.Doc.Parser.ignoreFn p c s = (p c s).shrinkStack s.stxStack.size

def Lean.Doc.Parser.lineTailWsFn : Parser.ParserFn

Consumes the whitespace that separates a block from what follows it: the rest of the current line, any blank lines, and the indentation of the line where content resumes.

Tabs are not valid whitespace characters, so they are not consumed. The next block actually throws the error.

Equations

• Lean.Doc.Parser.lineTailWsFn = Lean.Parser.takeWhileFn fun (ch : Char) => ch == ' ' || ch == '\n'

def Lean.Doc.Parser.asTokenFn (p : Parser.ParserFn) (trailing : Parser.ParserFn := skipFn) : Parser.ParserFn

Matches an arbitrary parser and pushes the consumed input as a Syntax.atom. The trailing parser runs after the token's content, and the input it consumes becomes the token's trailing whitespace.

Equations

• Lean.Doc.Parser.asTokenFn p trailing c s = if (p c s).hasError = true then p c s else Lean.Doc.Parser.asTokenAux✝ trailing s.pos c ((p c s).shrinkStack s.stxStack.size)

inductive Lean.Doc.Parser.OrderedListType : Type

Ordered lists may have two styles of marker, with trailing dots or parentheses.

• numDot : OrderedListType

  Items like 1.

• parenAfter : OrderedListType

  Items like 1)

def Lean.Doc.Parser.instReprOrderedListType.repr : OrderedListType → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Doc.Parser.instReprOrderedListType : Repr OrderedListType

Equations

• Lean.Doc.Parser.instReprOrderedListType = { reprPrec := Lean.Doc.Parser.instReprOrderedListType.repr }

def Lean.Doc.Parser.instBEqOrderedListType.beq : OrderedListType → OrderedListType → Bool

Equations

• Lean.Doc.Parser.instBEqOrderedListType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Lean.Doc.Parser.instBEqOrderedListType : BEq OrderedListType

Equations

• Lean.Doc.Parser.instBEqOrderedListType = { beq := Lean.Doc.Parser.instBEqOrderedListType.beq }

@[instance_reducible]

instance Lean.Doc.Parser.instDecidableEqOrderedListType : DecidableEq OrderedListType

Equations

• Lean.Doc.Parser.instDecidableEqOrderedListType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lean.Doc.Parser.instOrdOrderedListType : Ord OrderedListType

Equations

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

inductive Lean.Doc.Parser.UnorderedListType : Type

Unordered lists may have three markers: asterisks, dashes, or pluses.

• asterisk : UnorderedListType

  Items like *

• dash : UnorderedListType

  Items like -

• plus : UnorderedListType

  Items like +

@[instance_reducible]

instance Lean.Doc.Parser.instReprUnorderedListType : Repr UnorderedListType

Equations

• Lean.Doc.Parser.instReprUnorderedListType = { reprPrec := Lean.Doc.Parser.instReprUnorderedListType.repr }

def Lean.Doc.Parser.instReprUnorderedListType.repr : UnorderedListType → Nat → Format

Equations

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

def Lean.Doc.Parser.instBEqUnorderedListType.beq : UnorderedListType → UnorderedListType → Bool

Equations

• Lean.Doc.Parser.instBEqUnorderedListType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Lean.Doc.Parser.instBEqUnorderedListType : BEq UnorderedListType

Equations

• Lean.Doc.Parser.instBEqUnorderedListType = { beq := Lean.Doc.Parser.instBEqUnorderedListType.beq }

@[instance_reducible]

instance Lean.Doc.Parser.instDecidableEqUnorderedListType : DecidableEq UnorderedListType

Equations

• Lean.Doc.Parser.instDecidableEqUnorderedListType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lean.Doc.Parser.instOrdUnorderedListType : Ord UnorderedListType

Equations

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

def Lean.Doc.Parser.inlineTextCharFn : Parser.ParserFn

Parses a character that's allowed as part of inline text. This resolves escaped characters and performs limited lookahead for characters that only begin a different inline as part of a sequence.

Equations

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

def Lean.Doc.Parser.blockOpenerFn : Parser.ParserFn

Parses block opener prefixes. If this parser succeeds at the beginning of a line, then a special block is beginning.

Equations

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

def Lean.Doc.Parser.valFn (trailing : Parser.ParserFn := skipFn) : Parser.ParserFn

Parses an argument value, which may be a string, an identifier, or a numeral. The value's token records the input consumed by trailing as its trailing whitespace.

Equations

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

def Lean.Doc.Parser.recoverBlockAtErrPos (p : Parser.ParserFn) : Parser.ParserFn

Runs p, and on failure consumes input with recover until parsing may continue. The error is recorded where p stopped, so that it marks the input that could not be read rather than the input that recovery passed over.

Equations

• Lean.Doc.Parser.recoverBlockAtErrPos p = Lean.Doc.Parser.recoverAtErrPos✝ p (Lean.Doc.Parser.ignoreFn Lean.Doc.Parser.skipBlock✝)

def Lean.Doc.Parser.argEndWs : Parser.ParserFn

The whitespace after an argument, recorded on the argument's last token as its trailing whitespace: the spaces that follow it.

Equations

• Lean.Doc.Parser.argEndWs = Lean.Doc.Parser.eatSpaces✝

def Lean.Doc.Parser.argFn (tail : Parser.ParserFn := skipFn) (closes : Char → Bool := fun (x : Char) => false) : Parser.ParserFn

Parses an argument to a role, directive, command, or code block, which may be named or positional or a flag. The argument's final token records the input tail consumes as its trailing whitespace.

Error recovery stops at characters that satisfy closes, which should delimit the current argument list (e.g. via a role's }).

Equations

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

def Lean.Doc.Parser.argsFn (tail : Parser.ParserFn := argEndWs) (closes : Char → Bool := fun (x : Char) => false) : Parser.ParserFn

Parses zero or more arguments to a role, directive, command, or code block. Each argument's final token records the input tail consumes as its trailing whitespace. The argument list must be on the line the parser starts on. A starting position at the beginning of a line means the list has already ended, so the list is empty.

Error recovery stops at characters that satisfy closes, which should delimit the current argument list (e.g. via a role's }).

Equations

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

def Lean.Doc.Parser.nameAndArgsFn (tail : Parser.ParserFn := argEndWs) (closes : Char → Bool := fun (x : Char) => false) : Parser.ParserFn

Parses a name and zero or more arguments to a role, directive, command, or code block. The final token of the name and of each argument records the input that tail consumes as its trailing whitespace. The name and arguments must be on the line the parser starts on. A starting position at the beginning of a line fails to parse a name.

The caller's own tokens record the whitespace before the name. If a caller lets this parser consume that whitespace instead, no token records it.

Error recovery stops at characters that satisfy closes, which should delimit the current argument list (e.g. via a role's }).

Equations

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

structure Lean.Doc.Parser.InlineCtxt : Type

The context within which a newline element is parsed.

• allowNewlines : Bool

  Are newlines allowed here?

• boldDepth : Option Nat

  How many asterisks introduced the current level of boldness? none means no bold here.

• emphDepth : Option Nat

  How many underscores introduced the current level of emphasis? none means no emphasis here.

• inLink : Bool

  Are we in a link?

• tail : Parser.ParserFn

  The trailing whitespace parser for the final token of a top-level inline element.

• baseColumn : Nat

  The docstring's base column, which allows inline code and math to be parsed relative to the docstring's indentation.

@[instance_reducible]

instance Lean.Doc.Parser.instInhabitedInlineCtxt : Inhabited InlineCtxt

Equations

• Lean.Doc.Parser.instInhabitedInlineCtxt = { default := Lean.Doc.Parser.instInhabitedInlineCtxt.default }

partial def Lean.Doc.Parser.emphFn (ctxt : InlineCtxt) : Parser.ParserFn

Parses emphasis: a matched pair of one or more _.

partial def Lean.Doc.Parser.boldFn (ctxt : InlineCtxt) : Parser.ParserFn

Parses bold: a matched pair of one or more *.

def Lean.Doc.Parser.codeFn (ctxt : InlineCtxt := { }) : Parser.ParserFn

Parses inline code. The content is one versoCodeLine token per source line. Each line's token records the docstring's indentation on the line after it as trailing whitespace, while indentation past that column is part of the code. A space written at each end of the content to escape a backtick or a space becomes whitespace on the token before it.

Equations

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

def Lean.Doc.Parser.mathFn (ctxt : InlineCtxt := { }) : Parser.ParserFn

Parses mathematics. The content is inline code, with its lines and indentation read the same way.

Equations

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

def Lean.Doc.Parser.textFn (ctxt : InlineCtxt := { }) : Parser.ParserFn

Reads a prefix of a line of text, stopping at a text-mode special character.

Equations

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

partial def Lean.Doc.Parser.linkFn (ctxt : InlineCtxt) : Parser.ParserFn

Parses a link.

def Lean.Doc.Parser.footnoteFn (ctxt : InlineCtxt) : Parser.ParserFn

Parses a footnote.

Equations

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

def Lean.Doc.Parser.imageFn (tail : Parser.ParserFn := skipFn) : Parser.ParserFn

Parses an image.

Equations

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

partial def Lean.Doc.Parser.roleFn (ctxt : InlineCtxt) : Parser.ParserFn

Parses a role.

partial def Lean.Doc.Parser.delimitedInlineFn (ctxt : InlineCtxt) : Parser.ParserFn

Parses an inline that is self-delimiting (that is, with well-defined start and stop characters).

partial def Lean.Doc.Parser.inlineFn (ctxt : InlineCtxt) : Parser.ParserFn

Parses any inline element.

def Lean.Doc.Parser.textLineFn (ctxt : InlineCtxt := { }) (recordTrailing : Bool := false) : Parser.ParserFn

Parses a line of text (that is, one or more inline elements). When recordTrailing is set, each top-level inline's final token consumes the whitespace that follows it as its trailing whitespace.

Equations

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

def Lean.Doc.Parser.metadataContents : Parser.Parser

The fields of a metadata block, which are the fields of a structure instance.

Equations

• Lean.Doc.Parser.metadataContents = Lean.Parser.Term.structInstFields (Lean.Parser.sepByIndent Lean.Parser.Term.structInstField ", " (Lean.Parser.symbol ", ") true)

inductive Lean.Doc.Parser.ListStyle : Type

The style of a list, shared by all of its items.

• ordered (type : OrderedListType) : ListStyle

  A list whose items are numbered.

• unordered (type : UnorderedListType) : ListStyle

  A list whose items are bulleted.

structure Lean.Doc.Parser.BlockCtxt : Type

The context within which a block should be valid.

• topLevel : Bool

  Whether blocks in this context are at the document's top level, rather than the contents of another block.

• recordTrailing : Bool

  Whether each block's final token records the whitespace that follows the block as its trailing whitespace.

• maxDirective : Option Nat

  The block's maximal directive size (that is, the greatest number of allowed colons).

• docStartPosition : Position

  The position at which the document content starts, used to allow headers on the first line of a docstring (e.g. /-! # Header -/). With the default value ⟨1, 0⟩, the beginning-of-line check is unaffected for normal documents.

• baseColumn : Nat

  The base column of the docstring, which is the least indentation of any non-empty line in it, including the opening and closing delimiters. Items that may not nest in blocks, such as headers, start at this column, and a code element's lines treat the indentation up to it as whitespace.

@[instance_reducible]

instance Lean.Doc.Parser.instInhabitedBlockCtxt : Inhabited BlockCtxt

Equations

• Lean.Doc.Parser.instInhabitedBlockCtxt = { default := Lean.Doc.Parser.instInhabitedBlockCtxt.default }

@[instance_reducible]

instance Lean.Doc.Parser.instReprBlockCtxt : Repr BlockCtxt

Equations

• Lean.Doc.Parser.instReprBlockCtxt = { reprPrec := Lean.Doc.Parser.instReprBlockCtxt.repr }

def Lean.Doc.Parser.instReprBlockCtxt.repr : BlockCtxt → Nat → Format

Equations

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

def Lean.Doc.Parser.BlockCtxt.forDocString (text : FileMap) (openPos startPos endPos : String.Pos.Raw) : BlockCtxt

Computes the BlockCtxt for parsing a docstring whose opening delimiter is at openPos and whose content begins at startPos, on the line where that content starts and separated from it by spaces alone. endPos is the position of the - before the / in the closing delimiter.

When the docstring content starts mid-line (e.g. /-! # Header -/), the docStartPosition is set to the position after any leading spaces so that headers on the first line are recognized. For indented docstrings, baseColumn is computed as the minimum column among the opening delimiter, the closing delimiter, and the least-indented non-empty content line.

Equations

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

def Lean.Doc.Parser.metadataBlockFn (ctxt : BlockCtxt := { }) : Parser.ParserFn

Parses a metadata block, which contains the contents of a Lean structure initialization but is surrounded by %%% on each side.

Equations

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

def Lean.Doc.Parser.lookaheadOrderedListMarker (p : OrderedListType → Int → Parser.ParserFn) : Parser.ParserFn

Succeeds when the parser is looking at an ordered list marker.

Equations

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

def Lean.Doc.Parser.lookaheadUnorderedListMarker (p : UnorderedListType → Parser.ParserFn) : Parser.ParserFn

Succeeds when the parser is looking at an unordered list marker.

Equations

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

def Lean.Doc.Parser.setStartLeading (startPos : String.Pos.Raw) (stx : Syntax) : Syntax

Sets the leading whitespace of the first token in stx to run from startPos. Syntax without tokens stays unchanged.

Every token that a parse produces has empty leading whitespace, because the token before it records the whitespace between them. The first token of an input records the whitespace that the input starts with, and this applies it.

Equations

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

partial def Lean.Doc.Parser.listItemFn (ctxt : BlockCtxt) (style : ListStyle) : Parser.ParserFn

Parses an item of a list in the given style. The saved position is the first item marker's, which every marker lines up with.

partial def Lean.Doc.Parser.descItemFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses an item from a description list. The saved position is the first item's colon, which every item's colon lines up with.

partial def Lean.Doc.Parser.blockquoteFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses a block quote.

partial def Lean.Doc.Parser.unorderedListFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses an unordered list.

partial def Lean.Doc.Parser.orderedListFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses an ordered list.

partial def Lean.Doc.Parser.definitionListFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses a definition list.

def Lean.Doc.Parser.paraFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses a paragraph (that is, a sequence of otherwise-undecorated inlines). A paragraph contains something other than whitespace, so a run of empty lines is not a paragraph.

Equations

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

def Lean.Doc.Parser.headerFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses a header.

Equations

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

def Lean.Doc.Parser.codeBlockFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses a code block. Each line's token records the fence's indentation on the line after it as trailing whitespace, so the code the block denotes is what the lines' tokens contain.

Equations

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

partial def Lean.Doc.Parser.directiveFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses a directive.

def Lean.Doc.Parser.blockCommandFn (ctxt : BlockCtxt) : Parser.ParserFn

Parses a block command.

Equations

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

def Lean.Doc.Parser.linkRefFn (c : BlockCtxt) : Parser.ParserFn

Parses a link reference target.

Equations

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

def Lean.Doc.Parser.footnoteRefFn (c : BlockCtxt) : Parser.ParserFn

Parses a footnote reference target.

Equations

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

partial def Lean.Doc.Parser.blockFn (c : BlockCtxt) : Parser.ParserFn

Parses a block.

When recordTrailing is set, the block's final token consumes the whitespace that follows the block (including the indentation of the next line), even when error recovery lost the token that would have consumed it.

partial def Lean.Doc.Parser.blocksFn (c : BlockCtxt) : Parser.ParserFn

Parses zero or more blocks. Each block's final token consumes the whitespace that follows it, the next line's indentation included, and blockSepFallback parses the whitespace after a block whose final token was lost to error recovery.

partial def Lean.Doc.Parser.blocks1Fn (c : BlockCtxt) : Parser.ParserFn

Parses one or more blocks.

def Lean.Doc.Parser.documentFn (blockContext : BlockCtxt := { }) : Parser.ParserFn

Parses a document: the whitespace it starts with, then zero or more blocks.

The document's first token records the whitespace between the position where this parser starts and that token. A caller that starts it part-way into a larger input is responsible for the whitespace before that position, which a doc comment's opening delimiter records as its trailing whitespace.

Equations

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

def Lean.Doc.Parser.locateError (ictx : Parser.InputContext) (pos : String.Pos.Raw) (e : Parser.Error) : String.Pos.Raw × Option String.Pos.Raw × Parser.Error

Returns the start and end of the range over which a Verso parse error at pos is reported, along with the error to report. An end position of none indicates that the error has no range, but is to be reported at a single point.

An error that includes an unexpected token is reported at that token's range. When such an error has no message of its own, as with errors from Lean's own parsers, a message is derived from the token.

Otherwise, the range starts at pos and covers the character there, or the whole run of it when a Verso element repeats that character to make a single delimiter (e.g. *** for bold text). At the end of the input, and at a newline, the end is none.

Whitespace before the error stays outside the range.

Equations

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

def Lean.Doc.Parser.documentKinds : List SyntaxNodeKind

The syntax kinds of the nodes that documentFn produces.

Equations

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

def Lean.Doc.Parser.documentInfo : Parser.ParserInfo

Parser information for Verso markup.

Listing the syntax kinds that documentFn produces ensures that we don't get spurious module dependencies.

Equations

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

def Lean.Doc.Parser.ifVersoFn (ifVerso ifNotVerso : Parser.ParserFn) : Parser.ParserFn

Parses as ifVerso if the option doc.verso is true, or as ifNotVerso otherwise.

Equations

• Lean.Doc.Parser.ifVersoFn ifVerso ifNotVerso c s = if c.options.getBool `doc.verso = true then ifVerso c s else ifNotVerso c s

def Lean.Doc.Parser.ifVerso (ifVerso ifNotVerso : Parser.Parser) : Parser.Parser

Parses as ifVerso if the option doc.verso is true, or as ifNotVerso otherwise.

Equations

• Lean.Doc.Parser.ifVerso ifVerso ifNotVerso = { info := Lean.Parser.orelseInfo ifVerso.info ifNotVerso.info, fn := Lean.Doc.Parser.ifVersoFn ifVerso.fn ifNotVerso.fn }

def Lean.Doc.Parser.ifVerso.formatter (f1 f2 : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

Formatter for ifVerso—formats according to the underlying formatters.

Equations

• Lean.Doc.Parser.ifVerso.formatter f1 f2 = (f1 <|> f2)

def Lean.Doc.Parser.ifVerso.parenthesizer (p1 p2 : PrettyPrinter.Parenthesizer) : PrettyPrinter.Parenthesizer

Parenthesizer for ifVerso—parenthesizes according to the underlying parenthesizers.

Equations

• Lean.Doc.Parser.ifVerso.parenthesizer p1 p2 = (p1 <|> p2)

def Lean.Doc.Parser.ifVersoModuleDocsFn (ifVerso ifNotVerso : Parser.ParserFn) : Parser.ParserFn

Parses as ifVerso if module docs should use Verso syntax, or as ifNotVerso otherwise. Checks doc.verso.module if explicitly set, otherwise falls back to doc.verso.

Equations

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

def Lean.Doc.Parser.ifVersoModuleDocs (ifVerso ifNotVerso : Parser.Parser) : Parser.Parser

Parses as ifVerso if module docs should use Verso syntax, or as ifNotVerso otherwise. Checks doc.verso.module if explicitly set, otherwise falls back to doc.verso.

Equations

• Lean.Doc.Parser.ifVersoModuleDocs ifVerso ifNotVerso = { info := Lean.Parser.orelseInfo ifVerso.info ifNotVerso.info, fn := Lean.Doc.Parser.ifVersoModuleDocsFn ifVerso.fn ifNotVerso.fn }

def Lean.Doc.Parser.ifVersoModuleDocs.formatter (f1 f2 : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

Formatter for ifVersoModuleDocs—formats according to the underlying formatters.

Equations

• Lean.Doc.Parser.ifVersoModuleDocs.formatter f1 f2 = (f1 <|> f2)

def Lean.Doc.Parser.ifVersoModuleDocs.parenthesizer (p1 p2 : PrettyPrinter.Parenthesizer) : PrettyPrinter.Parenthesizer

Parenthesizer for ifVersoModuleDocs—parenthesizes according to the underlying parenthesizers.

Equations

• Lean.Doc.Parser.ifVersoModuleDocs.parenthesizer p1 p2 = (p1 <|> p2)

def Lean.Doc.Parser.withoutVersoSyntax (p : Parser.Parser) : Parser.Parser

Disables the option doc.verso while running a parser.

Equations

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

def Lean.Doc.Parser.withoutVersoSyntax.formatter (p : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

Formatter for withoutVersoSyntax—formats according to the underlying formatter.

Equations

• Lean.Doc.Parser.withoutVersoSyntax.formatter p = p

def Lean.Doc.Parser.withoutVersoSyntax.parenthesizer (p : PrettyPrinter.Parenthesizer) : PrettyPrinter.Parenthesizer

Parenthesizer for withoutVersoSyntax—parenthesizes according to the underlying parenthesizer.

Equations

• Lean.Doc.Parser.withoutVersoSyntax.parenthesizer p = p