Crate documents 

The rules of a document a person reads and edits through a page: which version it is, which characters its bytes spell, where its blocks lie, how much of it one answer carries, what one save changes, how a suggestion about it is read and decided, and how a Markdown window reads (crates/documents/Spec.lean).

No I/O: the bytes arrive as slices and leave as values. Reading the disk and the content store, and recording a save, belong to the crates that own those (D1).

Structs

Applied

What applying a transaction left: the new version’s bytes and identity, and the transaction that takes it back.

Edit

One replacement: the bytes of span in the baseline become bytes.

Laid

A stretch of Markdown that was read, and its blocks: what a preview and a reply both answer (D32). An empty stretch has none.

Lifted

Bytes lifted out of a version so a window can be cut from them.

ListItem

One item of a list, with the blocks inside it.

Offer

One proposal as the Ledger offered it: who offered it, about which stretch of which version, and the two texts (D13, D18).

Review

The card two texts make: their sentences aligned in reading order.

Row

One row of a table: one run of inline marks per cell.

Selection

Where a selection was begun and where it was carried to, as byte offsets of one version; collapsed when the two are the same offset.

Slice

One sentence of a card with the whitespace around it; lead, text and trail read in order are the sentence’s bytes (D14).

Span

A half-open byte interval [start, end) of one document version.

TextEdit

One edit as a page sends it: a stretch of the baseline’s bytes, and the text that takes its place (D11).

Transaction

Edits against one version, in order, none overlapping another.

Window

One stretch of a version, and the characters it spells.

Enums

Align

How a table column is aligned.

Block

One block of a window, with the bytes of the version it was read from (D26).

Check

Whether an item is a task, and whether it is done.

Construct

What a page is shown the source of instead of a drawing (D22, D24).

Encoding

The character encoding one document version is read in.

Format

The grammar a document’s blocks are read by.

Inline

One inline mark. Inline marks carry no span: the readers of today line a preview up with its source block by block (D26).

Order

Whether a list counts its items, and from where.

Preview

One window of a Markdown version, laid out, or the reason it was not.

Reading

What one version’s bytes are to a reader.

ReplyState

Whether a model’s reply is still arriving (D30).

SliceKind

The role one sentence plays on a card.

Spacing

Whether a list’s items are paragraphs apart or one line apart.

Constants

ALIGN_CELLS_MAX

How many cells the common-subsequence table may hold: u32 each, sixteen MiB in all (D15). Past it the middle of the two lists is one deletion and one insertion: still exact, only coarser.

EXPORT_BYTES_MAX

The longest version one export reads: an export’s HTML, about twice its source, still travels as one answer.

PROPOSAL_ID_TAG

What a proposal’s identity digest begins with, so it is never the digest of some document that happens to hold the same bytes (D13).

WINDOW_BYTES_MAX

The most bytes one window carries past the offset it was asked from.

Functions

cut

The window wanted asks for, cut from bytes lift named.

decide

Decides several cards on one document at once: what their verdicts accept lands on source as one save, and None when they accept nothing (D17).

export

bytes, a Markdown version in encoding, as one HTML file titled title.

head

The first window of a whole version.

lift

The bytes to lift out of a version of size bytes to cut the window wanted asks for: up to [REACH] bytes before it, so a start inside a character can step back to that character, and up to [REACH] after its bounded end, so the end can tell whether a character runs on past it.

preview

The preview of the window viewport asks for, cut from bytes lift named.

reply

The blocks of a model’s reply that can no longer change, read by the grammar a preview is (D30): a settled reply is read as a version holding exactly its text, one still streaming only up to its closure point (D31). At most one window, as a preview; span.end is where the rest of the text is sent from.

save

Applies a page’s text edits to source, which must be the version baseline, writing each text in that version’s encoding (D11, D12).