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

A parser that does nothing.

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

Parses as p, but discards the result.

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.

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.

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)

@[implicit_reducible]

instance Lean.Doc.Parser.instReprOrderedListType : Repr OrderedListType

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

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

@[implicit_reducible]

instance Lean.Doc.Parser.instBEqOrderedListType : BEq OrderedListType

@[implicit_reducible]

instance Lean.Doc.Parser.instDecidableEqOrderedListType : DecidableEq OrderedListType

@[implicit_reducible]

instance Lean.Doc.Parser.instOrdOrderedListType : Ord OrderedListType

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 +

@[implicit_reducible]

instance Lean.Doc.Parser.instReprUnorderedListType : Repr UnorderedListType

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

@[implicit_reducible]

instance Lean.Doc.Parser.instBEqUnorderedListType : BEq UnorderedListType

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

@[implicit_reducible]

instance Lean.Doc.Parser.instDecidableEqUnorderedListType : DecidableEq UnorderedListType

@[implicit_reducible]

instance Lean.Doc.Parser.instOrdUnorderedListType : Ord UnorderedListType

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.

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.

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

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

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.

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.

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

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

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.

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

@[implicit_reducible]

instance Lean.Doc.Parser.instInhabitedInlineCtxt : Inhabited InlineCtxt

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.

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

Parses mathematics.

def Lean.Doc.Parser.text : Parser.ParserFn

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

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.

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

Parses an image.

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.

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

@[implicit_reducible]

instance Lean.Doc.Parser.instReprInList : Repr InList

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

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

@[implicit_reducible]

instance Lean.Doc.Parser.instInhabitedBlockCtxt : Inhabited BlockCtxt

@[implicit_reducible]

instance Lean.Doc.Parser.instReprBlockCtxt : Repr BlockCtxt

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

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.

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.

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.

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

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

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

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

Parses a header.

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.

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.

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

Parses a link reference target.

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

Parses a footnote reference target.

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.

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.

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.

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

Formatter for ifVerso—formats according to the underlying formatters.

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

Parenthesizer for ifVerso—parenthesizes according to the underlying parenthesizers.

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.

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.

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

Formatter for ifVersoModuleDocs—formats according to the underlying formatters.

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

Parenthesizer for ifVersoModuleDocs—parenthesizes according to the underlying parenthesizers.

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

Disables the option doc.verso while running a parser.

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

Formatter for withoutVersoSyntax—formats according to the underlying formatter.

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

Parenthesizer for withoutVersoSyntax—parenthesizes according to the underlying parenthesizer.