The lines of a derivation that a substitution makes
A rewrite entity makes the LaTeX of a new line from the LaTeX of an old
line. expand/1 reads the old line with Expresso.Element.Math.Latex and
walks its atoms:
- An occurrence of
replacebecomes the new content:\from{name}{…}with the LaTeX of the partby, or the LaTeX ofby_tex. - A part of
dropgoes away. - A run of other atoms in one group becomes
\part{keep-k-n}{…}in the old line and\from{keep-k-n}{…}in the new line, so it moves down at the step of the new line.kis the number of the new line. - A group or a command that holds an occurrence or a part of
dropstays, and the walk goes into it. In the new line, it fades in.
Each occurrence also gets \class{hit-k}{…} in the old line. The new line
has 3 steps by default, one for each phase: at :occurrences, the
occurrences and the source of by get a color; at :kept, the kept runs
move; at :copies, the copies of by move. The steps option puts phases
together in one step. Without why, the reason is replace := by in LaTeX.
The links of Expresso.Element.Math.Links and the copies of
Expresso.Element.Copy then move the symbols. docs/line-rewrites.md gives
the design.
Summary
Functions
Turn each rewrite of a list of lines into a line
Functions
@spec expand([Expresso.Element.MathLine.t() | Expresso.Element.MathRewrite.t()]) :: {:ok, [Expresso.Element.MathLine.t()]} | {:error, String.t()}
Turn each rewrite of a list of lines into a line
The function returns the lines in order. A rewrite also changes its old
line, because each kept run of the old line gets a \part. It returns an
error for a rewrite with no line before it, for a name that the old line or
an earlier line does not have, and for a rewrite with no occurrence.