Djot.SourceA djot text together with its parse, for texts that change.
An edit gives a new source whose document equals Doc.of_string on the edited text, parsing again only the part of the text the edit can affect. A value of type t is immutable: the source before an edit stays valid.
Edit the source, not the document: doc is always the parse of to_string, so a document changed with Mapper.map_doc has to be mapped again after an edit. To make a changed document the text to edit, start a new source from Doc.to_string.
of_string s is the source with text s. profile, locs and frontmatter are as in Doc.of_string, and hold for every edit of this source.
With frontmatter, an edit after the frontmatter parses as any edit does. An edit that reaches the frontmatter, or the start of a text without one, can make, change or unmake it; when it does, the whole text is parsed again and the change is every line.
val to_string : t -> stringThe text. Doc.textloc of doc gives byte ranges in it.
The parse of the text, equal to Doc.of_string on to_string.
replace_lines t ~first ~last s is t with lines first to last of its text replaced by s. Lines are counted from one and both ends are included, so ~first:2 ~last:3 replaces two lines.
With last = first - 1 no line is replaced and s is inserted before line first: ~first:1 ~last:0 inserts at the start, and with n lines in the text ~first:(n + 1) ~last:n appends. This is the empty range of Textloc.is_empty.
s is taken as whole lines: a newline is added where s would otherwise join a neighbouring line.
replace_bytes t ~first ~last s is t with bytes first to last of its text replaced by exactly s. Bytes are counted from zero and both ends are included, as in Textloc. With last = first - 1 no byte is replaced and s is inserted before byte first.
The lines an edit parsed again, one-based and inclusive: lines first to old_last of the text before the edit, which are lines first to new_last of the text after it. A last line of first - 1 is an empty range. The range holds the edited lines and can be wider.
The lines outside it were not parsed: the blocks they give are the ones of the document before the edit, with the positions of those after the range moved. Identifiers, sections, footnotes and references are still worked out over the whole document, so outside the range an edit can change the suffix of a repeated heading identifier, where a section ends, and what Doc.reference and Doc.footnote answer.
replace_lines, with the lines it parsed again.
replace_bytes, with the lines it parsed again.