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

A parser that does nothing.

Equations

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
instance Lean.Doc.Parser.instReprOrderedListType :
Repr OrderedListType
Equations

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

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

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

Instances For

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

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

Instances For

source
instance Lean.Doc.Parser.instBEqOrderedListType :
BEq OrderedListType
Equations

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

source
instance Lean.Doc.Parser.instDecidableEqOrderedListType :
DecidableEq OrderedListType
Equations

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

source
instance Lean.Doc.Parser.instOrdOrderedListType :
Ord OrderedListType
Equations

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

source
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 +

Instances For

source
instance Lean.Doc.Parser.instReprUnorderedListType :
Repr UnorderedListType
Equations

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

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

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

Instances For

source
instance Lean.Doc.Parser.instBEqUnorderedListType :
BEq UnorderedListType
Equations

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

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

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

Instances For

source
instance Lean.Doc.Parser.instDecidableEqUnorderedListType :
DecidableEq UnorderedListType
Equations

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

source
instance Lean.Doc.Parser.instOrdUnorderedListType :
Ord UnorderedListType
Equations

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

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

source
instance Lean.Doc.Parser.instInhabitedInlineCtxt :
Inhabited InlineCtxt
Equations

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

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

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

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

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

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

Parses inline code.

Equations

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

Instances For

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

Parses mathematics.

Equations

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

Instances For

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

Instances For

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

Parses a link.

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

Instances For

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

Parses an image.

Equations

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

Instances For

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

Parses a role.

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

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

Parses any inline element.

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

Instances For

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

Equations

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

Instances For

source
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

Instances For

source
instance Lean.Doc.Parser.instReprInList :
Repr InList
Equations

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

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

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

Instances For

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

Instances For

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

- Lean.Doc.Parser.instInhabitedBlockCtxt.default = { minIndent := default, maxDirective := default, inLists := default }

Instances For

source
instance Lean.Doc.Parser.instInhabitedBlockCtxt :
Inhabited BlockCtxt
Equations

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

source
instance Lean.Doc.Parser.instReprBlockCtxt :
Repr BlockCtxt
Equations

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

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

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

Instances For

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

Instances For

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

Instances For

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

Parses a list item according to the current nesting context.

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

Parses an item from a description list.

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

Parses a block quote.

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

Parses an unordered list.

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

Parses an ordered list.

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

Parses a definition list.

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

Instances For

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

Instances For

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

Instances For

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

Parses a directive.

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

Instances For

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

Instances For

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

Instances For

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

Parses a block.

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

Parses zero or more blocks.

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

Parses one or more blocks.

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

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

Equations

- Lean.Doc.Parser.document blockContext = Lean.Doc.Parser.ignoreFn (Lean.Parser.manyFn Lean.Doc.Parser.blankLine✝) >> Lean.Doc.Parser.blocks blockContext

Instances For

source
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 Lean.KVMap.getBool c.options `doc.verso = true then ifVerso c s else ifNotVerso c s

Instances For

source
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 }

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For