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

A parser that does nothing.

Equations

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

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.asStringFn (p : Parser.ParserFn) (quoted : Bool := false) (transform : String → String := id) : Parser.ParserFn

Match an arbitrary Parser and return the consumed String in a Syntax.atom.

Equations

• Lean.Doc.Parser.asStringFn p quoted transform c s = if (p c s).hasError = true then p c s else Lean.Doc.Parser.asStringAux✝ quoted s.pos transform c ((p c s).shrinkStack s.stxStack.size)

def Lean.Doc.Parser.fakeAtom (str : String) (info : SourceInfo := SourceInfo.none) : Parser.ParserFn

Construct a “fake” atom with the given string content and source information.

Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is different enough from Lean's that this isn't always a good match.

Equations

• Lean.Doc.Parser.fakeAtom str info _c s = s.pushSyntax (Lean.Syntax.atom info str)

inductive Lean.Doc.Parser.OrderedListType : Type

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

• numDot : OrderedListType

  Items like 1.

• parenAfter : OrderedListType

  Items like 1)

@[instance_reducible]

instance Lean.Doc.Parser.instReprOrderedListType : Repr OrderedListType

Equations

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

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

Equations

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

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 indicators: 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.

@[instance_reducible]

instance Lean.Doc.Parser.instBEqUnorderedListType : BEq UnorderedListType

Equations

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

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.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.inlineTextChar : 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.blockOpener : Parser.ParserFn

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

Equations

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

def Lean.Doc.Parser.val : Parser.ParserFn

Parses an argument value, which may be a string literal, identifier, or numeric literal.

Equations

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

def Lean.Doc.Parser.recoverBlock (p : Parser.ParserFn) (final : Parser.ParserFn := skipFn) : Parser.ParserFn

Recovers from a parse error by skipping input until one or more complete blank lines has been skipped.

Equations

• Lean.Doc.Parser.recoverBlock p final = Lean.Parser.recoverFn p fun (x : Lean.Parser.RecoveryContext) => Lean.Doc.Parser.ignoreFn Lean.Doc.Parser.skipBlock✝ >> final

def Lean.Doc.Parser.arg : Parser.ParserFn

Parses an argument to a role, directive, command, or code block, which may be named or positional or a flag.

Equations

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

def Lean.Doc.Parser.args (multiline : Option Nat := none) : Parser.ParserFn

Parses zero or more arguments to a role, directive, command, or code block.

Equations

• Lean.Doc.Parser.args multiline = Lean.Parser.sepByFn true Lean.Doc.Parser.arg (Lean.Doc.Parser.nameArgWhitespace✝ multiline)

def Lean.Doc.Parser.nameAndArgs (multiline : Option Nat := none) : Parser.ParserFn

Parses a name and zero or more arguments to a role, directive, command, or code block.

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?

• minIndent : Nat

  The minimum indentation of a continuation line for the current paragraph

• 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?

def Lean.Doc.Parser.instInhabitedInlineCtxt.default : InlineCtxt

Equations

• Lean.Doc.Parser.instInhabitedInlineCtxt.default = { allowNewlines := default, minIndent := default, boldDepth := default, emphDepth := default, inLink := default }

@[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.emph (ctxt : InlineCtxt) : Parser.ParserFn

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

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

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

def Lean.Doc.Parser.code : Parser.ParserFn

Parses inline code.

Equations

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

def Lean.Doc.Parser.math : Parser.ParserFn

Parses mathematics.

Equations

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

def Lean.Doc.Parser.text : 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.link (ctxt : InlineCtxt) : Parser.ParserFn

Parses a link.

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

Parses a footnote.

Equations

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

def Lean.Doc.Parser.image : Parser.ParserFn

Parses an image.

Equations

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

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

Parses a role.

partial def Lean.Doc.Parser.delimitedInline (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.inline (ctxt : InlineCtxt) : Parser.ParserFn

Parses any inline element.

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

A non-meta copy of Lean.Doc.Syntax.metadataContents.

Equations

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

structure Lean.Doc.Parser.InList : Type

Records that the parser is presently parsing a list.

• indentation : Nat

  The indentation of list indicators.

• type : OrderedListType ⊕ UnorderedListType

  The specific list type and its indicator style

@[instance_reducible]

instance Lean.Doc.Parser.instReprInList : Repr InList

Equations

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

def Lean.Doc.Parser.instReprInList.repr : InList → Nat → Format

Equations

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

structure Lean.Doc.Parser.BlockCtxt : Type

The context within which a block should be valid.

• minIndent : Nat

  The block's minimum indentation.

• maxDirective : Option Nat

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

• inLists : List InList

  The nested list context, innermost first.

• 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. For indented docstrings (e.g. inside where blocks), beginning-of-line checks use this column instead of requiring column 0. With the default value 0, the check is equivalent to column == 0.

def Lean.Doc.Parser.instInhabitedBlockCtxt.default : BlockCtxt

Equations

• Lean.Doc.Parser.instInhabitedBlockCtxt.default = { minIndent := default, maxDirective := default, inLists := default, docStartPosition := default, baseColumn := default }

@[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) (startPos endPos : String.Pos.Raw) : BlockCtxt

Computes the BlockCtxt for parsing a docstring that starts at startPos in the given file map. endPos is the position of 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, 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.metadataBlock (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.lookaheadOrderedListIndicator (ctxt : BlockCtxt) (p : OrderedListType → Int → Parser.ParserFn) : Parser.ParserFn

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

Equations

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

def Lean.Doc.Parser.lookaheadUnorderedListIndicator (ctxt : BlockCtxt) (p : UnorderedListType → Parser.ParserFn) : Parser.ParserFn

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

Equations

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

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

Parses a list item according to the current nesting context.

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

Parses an item from a description list.

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

Parses a block quote.

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

Parses an unordered list.

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

Parses an ordered list.

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

Parses a definition list.

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

Parses a paragraph (that is, a sequence of otherwise-undecorated inlines).

Equations

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

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

Parses a header.

Equations

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

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

Parses a code block. The resulting string literal has already had the fences' leading indentation stripped.

Equations

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

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

Parses a directive.

def Lean.Doc.Parser.block_command (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.linkRef (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.footnoteRef (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.block (c : BlockCtxt) : Parser.ParserFn

Parses a block.

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

Parses zero or more blocks.

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

Parses one or more blocks.

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

Parses some number of blank lines followed by zero or more blocks.

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 = { 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 = { 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