Documentation with Verso

3.3. Traversal🔗

Because they are Lean values, Verso documents adhere to the structure of Lean programs in general. In particular, Lean doesn't support cyclic import graphs. It's common, however, for technical writing to include cyclic references; two sections that describe different aspects of something will frequently refer to one another. Similarly, a bibliography that's generated from a database needs a global view of a document to include only those works which are, in fact, cited.

The traversal phase occurs at runtime, before generating output. During the traversal phase, the document is repeatedly traversed from beginning to end, and metadata is accumulated into a table. The document may also be modified during traversal; this allows the title of a section to be inserted into a cross-reference. This traversal is repeated until the resulting document and metadata tables are not modified; it fails if a set number of passes are executed that result in modifications each time.

Verso provides a general-purpose traversal mechanism for Part, Block, and Inline that genres may use. Genre.TraverseState contains the genre-specific information that's accumulated during traversal, while Genre.TraverseContext provides a means of tracking the surrounding document context. To use this framework, genres should define instances of Traverse, which specifies the traversal of a genre's custom elements. Additionally, instances of GenrePart and GenreBlock specify how traversal keeps track of the current position in a document.

🔗type class
Verso.Doc.Traverse (g : Doc.Genre) (m : outParam (Type → Type)) : Type 1
Verso.Doc.Traverse (g : Doc.Genre)
  (m : outParam (Type → Type)) : Type 1

Genre-specific traversal.

The traversal pass is where cross-references are resolved. The traversal pass repeatedly applies a genre-specific stateful computation until a fixed point is reached, both with respect to the state and the document. Traversal may update the state or rewrite parts of the document.

The methods part, block, and inline provide effects to be carried out before traversing the given level of the AST, and part allows the part's metadata to be updated.

genrePart is carried out after part. It allows genre-specific rewriting of the entire part based on genre-specific metadata. This is typically used to construct a table of contents or permalinks, but it can in principle arbitrarily rewrite the part. inPart is used to locally transform the genre's traversal context along the lines of withReader, and can be used to keep track of e.g. the current position in the table of contents.

genreBlock and genreInline are invoked when traversal encounters Block.other and Inline.other. It may rewrite them, or have state effects.

Instance Constructor

Verso.Doc.Traverse.mk

Methods

part : [MonadReader g.TraverseContext m] → [MonadState g.TraverseState m] → Doc.Part g → m (Option g.PartMetadata)

The effects carried out before traversing a Part.

block : [MonadReader g.TraverseContext m] → [MonadState g.TraverseState m] → Doc.Block g → m Unit

The effects carried out before traversing a Block.

inline : [MonadReader g.TraverseContext m] → [MonadState g.TraverseState m] → Doc.Inline g → m Unit

The effects carried out before traversing an Inline.

genrePart : [MonadReader g.TraverseContext m] →
  [MonadState g.TraverseState m] → g.PartMetadata → Doc.Part g → m (Option (Doc.Part g))

Operations carried out after part, when a part has metadata. It allows genre-specific rewriting of the entire part based on genre-specific metadata. This is typically used to construct a table of contents or permalinks, but it can in principle arbitrarily rewrite the part. If it returns none, then no rewrite is performed.

genreBlock : [MonadReader g.TraverseContext m] →
  [MonadState g.TraverseState m] → g.Block → Array (Doc.Block g) → m (Option (Doc.Block g))

The traversal of genre-specific block values. If it returns none, then no rewrite is performed.

genreInline : [MonadReader g.TraverseContext m] →
  [MonadState g.TraverseState m] → g.Inline → Array (Doc.Inline g) → m (Option (Doc.Inline g))

The traversal of genre-specific inline values. If it returns none, then no rewrite is performed.

🔗type class
Verso.Doc.TraversePart (g : Doc.Genre) : Type
Verso.Doc.TraversePart (g : Doc.Genre) :
  Type

Specifies how to modify the context while traversing the contents of a given part.

Instance Constructor

Verso.Doc.TraversePart.mk

Methods

inPart : Doc.Part g → g.TraverseContext → g.TraverseContext

How to modify the context while traversing the contents of a given part. This is applied after part and genrePart have rewritten the text, if applicable.

It is also used during HTML generation.

🔗type class
Verso.Doc.TraverseBlock (g : Doc.Genre) : Type
Verso.Doc.TraverseBlock (g : Doc.Genre) :
  Type

Specifies how to modify the context while traversing the contents of a given block.

Instance Constructor

Verso.Doc.TraverseBlock.mk

Methods

inBlock : Doc.Block g → g.TraverseContext → g.TraverseContext

How to modify the context while traversing a given block.

It is also used during HTML generation.