Html

# Html Module Converts LaTeX AST nodes into HTML using Verso's `Html` type. This is the structured AST rendering path used for standalone LaTeX documents. ## Pipeline Position ``` Latex/Parser --> Latex.Block/Latex.Inline (AST) --> Html/Render --> Verso Html output ``` This module takes the parsed AST from `Latex/Parser.lean` and produces Verso `Html` values. It is one of two rendering paths in Runway: 1. **This path** (`Html/Render.lean`): Renders LaTeX AST directly to `Html` for standalone documents 2. **Traverse path** (`Traverse.lean` -> `Render.lean` -> `Theme.lean`): Loads Dress artifacts and renders chapter pages with side-by-side displays Both paths must handle the same node fields. When new fields are added to `NodeInfo` or `TheoremMetadata`, both paths need updating. ## File ### `Render.lean` The single file in this module. Key components: **Types:** - `RenderConfig`: Configuration for rendering -- base URL, MathJax toggle, CSS/JS file lists - `RenderState`: Tracks labels-to-IDs mapping, chapter/section numbering, per-environment theorem counters - `RenderM`: State monad (`StateM RenderState`) **Core Functions:** - `renderBlock`: Renders a single `Latex.Block` to `Html`. Handles all block types: documents, chapters, sections, theorems, proofs, paragraphs, math, lists, figures, and blueprint-specific commands - `renderInline`: Renders a single `Latex.Inline` to `Html`. Handles text, emphasis, bold, code, math, references, citations, links, images, and raw content - `renderPage`: Assembles a full HTML page with MathJax configuration, CSS links, and JS includes - `labelToId`: Converts LaTeX labels to valid HTML IDs - `registerLabel`: Records a label and returns its HTML ID - `nextTheoremNum`: Returns the next sequential number for a theorem environment type **Theorem Rendering:** Theorems are rendered into a CSS Grid-based side-by-side container (`sbs-container`) with three row pairs: 1. **Heading row**: Theorem type + number on the left, empty spacer on the right 2. **Statement row**: LaTeX statement on the left, Lean signature on the right 3. **Proof row**: LaTeX proof on the left, Lean proof body on the right Optional `above` and `below` content from `\leanabove` / `\leanbelow` commands are rendered as additional grid rows. **Blueprint-Specific Blocks:** The renderer produces placeholder `<div>` elements for commands that reference Lean declarations: - `\inputleanmodule{Module}` -> `<div class="lean-module" data-module="...">` - `\inputleannode{label}` -> `<div class="lean-node" data-label="...">` - `\paperstatement{label}` -> `<div class="paper-statement" data-label="...">` - `\paperfull{label}` -> `<div class="paper-full" data-label="...">` - `\paperproof{label}` -> `<div class="paper-proof" data-label="...">` These placeholders are later replaced with actual content by `Theme.replacePlaceholders`. **Top-Level API:** - `render`: Converts a `Latex.Document` to an HTML string - `renderToFile`: Renders and writes to a file path ## Math Rendering Inline math (`$...$`) is wrapped in `\( ... \)` delimiters. Display math (`$$...$$` or `\[...\]`) is wrapped in `\[ ... \]` inside a `div.math.display`. Both are left as-is for MathJax to process client-side. ## Image Handling Images from `\includegraphics` are resolved to `media/` paths. PDF images are automatically converted to `.png` extensions for web display. Images are rendered with `max-width: 100%`, `max-height: 70vh`, and lazy loading.