Typst documents: printing, parsing, and the round trip
printTyp
spells a canonical ESM document as Typst, parseTyp
reads it back, and
parseTyp_printTyp
is the round trip, composed exactly as for Markdown
(Esm.Document.Source.MarkdownDoc
) with the Typst math theorem parseTypst_printTypst.
Equations in Typst math
def prT (S : Sym) (e : Eqn) : String
An equation’s math text: its _comment as a // comment line, then the equation.
def oneT (S : Sym) (c : Option String) (body : List Char) : Option (List Eqn)
One display in Typst math: one equation, or (an accepted variant) several rows
separated by \ with & alignment, read by cookRows
(cookRows_layout
).
def ckT (S : Sym) (raw : String) : Option (List Eqn)
Read the math text of a display equation under the symbol table S.
def prTx : Sym → MC → MR
A math entry’s text: an equation’s Typst math (prT
), or a reaction with its rate
as Typst math.
What Typst spells natively
def capsT : Caps
The Typst container’s predicates: front-matter keys and attributes are named
arguments (identifiers that are not keywords); an equation’s Typst math must not contain
$ nor start with // (it may span lines: a code value inside an escape node does). Descriptions and component names are always
spellable (escapes).
The document
def headerT (front : List (String × Json)) : List Char
The header: the package import, then #show: esm-document.with(…) with the
front-matter entries.
def canonSegs (its : List RItem) : List Seg
The canonical layout: each construct after a blank line.
def lexDoc (s : List Char) : Option (List (String × Json) × List RItem)
Read the header and the constructs.
def parseTyp (s : String) : Option Json
Read a Typst document, after dropping a byte-order mark and reading CRLF line
endings as LF (decodeText
).
theorem decode_header (X : List Char) : decodeText (header ++ X) = header ++ X
A document with the header is read as written: decodeText
leaves it alone.
theorem lexDoc_front (front : List (String × Json)) (hf : ∀ a ∈ front, argOK a = true)
(segs : List Seg) (hv : Valid true segs) :
lexDoc (headerT front ++ render segs) = some (front, segItems segs)
The header and the body read back.
theorem items_ok (D : Doc MC) (h : DocOK capsT D) :
∀ it ∈ items (rawDoc prTx D), itemOK it = true
Every construct of the printed skeleton satisfies itemOK
.
theorem parseTyp_printTyp (d : Json) (hd : canonDoc d = true) : parseTyp (printTyp d) = some d
The Typst round trip. Every ESM document in canonical form reads back from its Typst spelling.
Prose and labels do not change the parse
theorem parseTyp_body (front : List (String × Json)) (hf : ∀ a ∈ front, argOK a = true)
(segs : List Seg) (hv : Valid true segs) :
parseTyp (String.ofList (headerT front ++ render segs)) = parseItemsT front (segItems segs)
The parse of a Typst document depends only on its front matter and its sequence of constructs: not on the prose between them, and not on equation labels.
theorem parseTyp_insert_prose (front : List (String × Json)) (hf : ∀ a ∈ front, argOK a = true)
(a b : List Seg) (p : List Char) (h₁ : Valid true (a ++ b)) (h₂ : Valid true (a ++ .prose p :: b)) :
parseTyp (String.ofList (headerT front ++ render (a ++ .prose p :: b))) =
parseTyp (String.ofList (headerT front ++ render (a ++ b)))
Inserting prose does not change the parse.
theorem parseTyp_label (front : List (String × Json)) (hf : ∀ a ∈ front, argOK a = true)
(a b : List Seg) (raw : String) (l : List Char) (h₁ : Valid true (a ++ .item (.eqn raw) :: b))
(h₂ : Valid true (a ++ .labeled raw l :: b)) :
parseTyp (String.ofList (headerT front ++ render (a ++ .labeled raw l :: b))) =
parseTyp (String.ofList (headerT front ++ render (a ++ .item (.eqn raw) :: b)))
Adding an equation label does not change the parse.