Documentation with Verso

3.1. Elaboration🔗

During the elaboration process, Verso's markup language is converted into its internal representation as a Lean inductive type. When Verso's elaborator encounters an extension point, it consults an internal table to select an implementation of the extension, and delegates to it. Other syntax is translated into the appropriate constructors of Verso's data.

All Verso documents are parameterized by their genre:

🔗structure
Verso.Doc.Genre : Type 1
Verso.Doc.Genre : Type 1

A genre is a kind of document that can be written with Verso.

A genre is primarily defined by its extensions to the Verso framework, provided in this type. Additionally, each genre should provide a main function that is responsible for the traversal pass and for generating output.

Constructor

Verso.Doc.Genre.mk

Fields

PartMetadata : Type

The metadata that may be associated with each Part (e.g. author, publication date, cross-referencing identifier).

Block : Type

Additional block-level values for documents written in the genre.

Inline : Type

Additional inline-level values for documents written in the genre.

TraverseContext : Type

The reader-style data used in the genre's traversal pass. Instances of TraversePart and TraverseBlock for a genre specify how this is updated while traversing parts and blocks, respectively.

TraverseState : Type

The mutable state used in the genre's traversal pass.

Each document consists of a Part. The part's title is the title of the entire document.

🔗def
Verso.Doc.Part (genre : Doc.Genre) : Type
Verso.Doc.Part (genre : Doc.Genre) : Type

A logical division of a document.

Parts contain Blocks:

🔗def
Verso.Doc.Block (genre : Doc.Genre) : Type
Verso.Doc.Block (genre : Doc.Genre) : Type

Block-level content in a document.

Blocks contain Inlines:

🔗def
Verso.Doc.Inline (genre : Doc.Genre) : Type
Verso.Doc.Inline (genre : Doc.Genre) :
  Type

Inline content that is part of the text flow.

The metadata field of Part typically gets its value from a metadata block written by the author, though it may be assigned more information during traversal. The Block.other and Inline.other constructors typically result from elaborating extension points.