LaTeX math: spelling and lexing of tokens
render
spells a token list as LaTeX math; lex
reads it back. Between two tokens
the renderer writes a space where the reader needs one (needSpace: a control word
or a letter before a letter, a number before a digit, . or e, a - before a
digit) and where it reads better (around binary operators, after commas, between
juxtaposed factors); the reader skips spaces. lex_render
is the lexer lemma:
every token list whose tokens are LaTeX tokens (tokOK
) reads back.
Spellings: numbers in the canonical spelling, scientific ones as
1.8 \times 10^{-12} (read back as one literal, with any spacing: 1.8\times10^{-12}
too; Esm.Document.Math.Surface
); a quantity’s unit as \,\mathrm{…} right after the
number, one token; \mathit{…}, \operatorname{…} and
\esm{…} hold their text with \, {, }, _, ^ escaped by a backslash;
\mathrm{…} and \text{…} hold raw balanced text; a JSON string (inside an escape
node’s fields) is \text{"…"}, its characters spelled by escS
(_, {, } with a
backslash, any character that is not plain printable ASCII as {\char NNN}), so it renders in
KaTeX’s text mode and is safe inside a Markdown math span. The earlier spelling, the string
double-quoted with JSON escapes in math mode, is still read.
Accepted on input and never written: \leq, \geq, \neq, \times, \bigl(,
\bigr), the spacing commands \;, \:, \!, \ , \quad, \qquad and \, (skipped
like spaces; \, is the unit separator only right before a \mathrm{…} that spells a
unit), and JSON numbers with an e exponent.
Spelling
def specials : List Char
Characters of a JSON string written as a hex escape in LaTeX.
def escCharB (c : Char) : List Char
The JSON escape of one character, with the specials as hex escapes.
def escCharL (c : Char) : List Char
The LaTeX spelling of one character of a JSON string: _ as \_ (so a renderer
that typesets the string does not read a subscript), otherwise escCharB
.
def fixUs : List Char → List Char
Undo the \_ of escCharL
up to the closing quote, leaving the other escapes and
everything after the quote alone.
def strPlain (c : Char) : Bool
A character of a JSON string written as itself inside \text{…}: printable ASCII
other than the characters TeX reads specially (keySpecial
, _, {, }).
def escS : List Char → List Char
The spelling of a JSON string’s characters inside \text{"…"}: a plain character as
itself, _, {, } with a backslash, and every other character as {\char NNN} (three
decimal digits below 1000, seven above). Every character renders in KaTeX’s text mode,
none is $ or a line break, and the braces balance.
def strL (s : String) : List Char
A JSON string in LaTeX: \text{"…"}, the characters spelled by escS
.
def textTok (raw : List Char) : Tok
The token of \text{raw}: a JSON string when the text is double-quoted, else text.
Spacing
def endsAlpha : Tok → Bool
t ends with letters a following letter would extend: a letter, a bare word, a
Greek name or a control word.
def merges (t : Tok) (c : Char) : Bool
A space is needed between t and a following token starting with c.
def pretty (p : Option Tok) (t1 t2 : Tok) : Bool
Spacing for reading: around binary operators (a - after an operand is binary),
after commas, colons and semicolons, and between juxtaposed operands (not before a call
parenthesis, and not before the [ of an index, k[1]).
Lexing
def ctrlKw : List (String × Kw)
Control words that are keywords, with the variants read on input.
def ctrlTok (w : String) (r : List Char) : Option (Tok × List Char)
After a control word: its token.
def skipSp : List Char → List Char
Skip white space and the two-character spacing commands, inside a scientific tail.
def sciExp (r : List Char) : Option (Int × List Char)
The scientific tail \times 10^{exponent} after a mantissa, with any spacing (none
included) between its parts.
def unitTok (r : List Char) : Option (List Esm.Units.Factor × List Char)
After \,: a unit \mathrm{…}, with white space between.
def lexOne (cs : List Char) : Option (Tok × List Char)
One token at the front of the input.
def skipWs : Nat → List Char → List Char
Skip spaces and the spacing commands (\, too, unless a unit follows it).