Module Djot

Djot documents: parse, traverse, render.

The tree types are the extracted ones from Kernel, re-exported with their constructors, so a value from the kernel and a value from this module are the same value. Every syntax extension is a constructor defined in the Rocq development; there are no extension points here.

module Kernel = Djot_kernel

Attributes

module Attr : sig ... end

Profiles

module Profile : sig ... end

Nodes

type 'a node = 'a Kernel.Ast.node =
  1. | Node of Kernel.Ast.pos * Attr.t * 'a
    (*

    A tree element: source position (see Doc.textloc), attributes, and contents.

    *)
module Node : sig ... end

Writing source

type style = [
  1. | `Safe
  2. | `Checked
  3. | `Naive
]

How a tree is written as djot source by to_string.

  • `Safe: text is escaped and delimiters are braced by fixed rules, so that the result parses back to the tree. Fast, and not what a person would type: 3\:1, {_a_}.
  • `Naive: the text a person would type, for a tree built by hand. Nothing is escaped, emphasis and quotes are written without braces where they read back as such, table columns are padded, and a blank line inside a container is empty. Text is written as it is, so a paragraph holding - x reads back as a list and a*b*c as strong emphasis.
  • `Checked: `Naive wherever that parses to the same tree as `Safe does, and `Safe for the top-level blocks where it does not. The result always parses as the `Safe one. Costs two parses of the result, more when blocks differ.

Inlines

module Inline : sig ... end

Blocks

module Block : sig ... end

Source locations

module Textloc : sig ... end

Frontmatter

module Frontmatter : sig ... end

YAML metadata at the start of a text, between two lines of ---:

Documents

module Doc : sig ... end

A parsed document: its blocks, and the footnotes and references they define.

Editable sources

module Source : sig ... end

A djot text together with its parse, for texts that change.

Streaming

module Stream : sig ... end

/*

module For_testing : sig ... end

/*

Traversals

module Mapper : sig ... end
module Folder : sig ... end

HTML

module Html : sig ... end