Renders a ShotUn.Trace as a Mermaid graph TD diagram.

Terms, substitutions and pair sides are rendered as LaTeX via ShotDs.Util.LatexFormatter and embedded inside a single $$…$$ math block per label. Multi-line labels use \begin{aligned}… \end{aligned} with an empty & at the head of each row for left alignment; prose (headers, "(empty σ)", …) lives inside \text{…}. All LaTeX fragments are maximally grouped in {…} so stray _, ^ or \lambda produced by the formatter bind only to the token they belong to.

Two renderer quirks are worked around at the label-generation layer, because Mermaid's Kino/Livebook pipeline hits them both:

• \\ row separators are halved. Mermaid's quoted-label parser treats \\ as an escape and emits a single \. That would collapse the KaTeX row break to a literal control-space. We emit \\\\ (four backslashes) so Mermaid halves it back to the \\ KaTeX expects.

• ~ and \ produce   in the KaTeX HTML. That entity is undefined in SVG's XML DTD and breaks "Save as SVG" downloads with error … Entity 'nbsp' not defined. Both are rewritten to \, (thin space, rendered via CSS margin, no HTML entity in the DOM).

<br/> HTML line breaks are not used — Mermaid drops them once the label parser hits $$…$$, collapsing everything onto one line. Everything lives inside the single math environment instead.

Edge styling mirrors ShotTx.Proof.to_mermaid/2: branching choice points (multiple children) use solid arrows (==>); linear continuations use dotted arrows (-.->). Node colours encode the node kind — start (blue), step (gray), solution (green), fail (orange).

Options

• :show_state — include the work-list (and accumulated σ for solution leaves) in each node's label. Defaults to true.