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)

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

instance Lean.Doc.Parser.instBEqOrderedListType : BEq OrderedListType

instance Lean.Doc.Parser.instDecidableEqOrderedListType : DecidableEq OrderedListType

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 +

instance Lean.Doc.Parser.instReprUnorderedListType : Repr UnorderedListType

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

instance Lean.Doc.Parser.instBEqUnorderedListType : BEq UnorderedListType

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

instance Lean.Doc.Parser.instDecidableEqUnorderedListType : DecidableEq UnorderedListType

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

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.

def Lean.Doc.Parser.metadataBlock : Parser.ParserFn

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

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

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

instance Lean.Doc.Parser.instInhabitedBlockCtxt : Inhabited BlockCtxt

instance Lean.Doc.Parser.instReprBlockCtxt : Repr BlockCtxt

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

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