From d3ed78bcd1b37aa2a0f1d20c80adbaa112138370 Mon Sep 17 00:00:00 2001 From: Roman-Manevich Date: Wed, 8 Jul 2026 19:42:18 +0100 Subject: [PATCH] improved HTML rendering of the ASL Reference with MathJax --- asllib/doc/Expressions.tex | 2 +- asllib/doc/Makefile | 20 +- asllib/doc/StandardLibrary.tex | 2 +- asllib/doc/hevea/README.md | 234 +++++ asllib/doc/hevea/asl-html.css | 259 +++++ asllib/doc/hevea/generate_mathjax_config.py | 1047 +++++++++++++++++++ asllib/doc/hevea/mathjax_config.hva | 12 + 7 files changed, 1571 insertions(+), 5 deletions(-) create mode 100644 asllib/doc/hevea/README.md create mode 100644 asllib/doc/hevea/asl-html.css create mode 100644 asllib/doc/hevea/generate_mathjax_config.py create mode 100644 asllib/doc/hevea/mathjax_config.hva diff --git a/asllib/doc/Expressions.tex b/asllib/doc/Expressions.tex index 91257f2626..cf7ecd387c 100644 --- a/asllib/doc/Expressions.tex +++ b/asllib/doc/Expressions.tex @@ -853,7 +853,7 @@ \subsection{Abstract Syntax} We refer to a \rhsexpression{} of the form \verb|b[[i]]|, where $b, i$ are subexpressions, as an \arrayaccessterm\ expression. We refer to $b$ and $i$ as the \emph{base} -and the $\emph{index}$ subexpressions, respectively. +and the \emph{index} subexpressions, respectively. \end{definition} \ExampleDef{Array Access Expressions} diff --git a/asllib/doc/Makefile b/asllib/doc/Makefile index 864ff8d30c..31d17f675d 100644 --- a/asllib/doc/Makefile +++ b/asllib/doc/Makefile @@ -3,6 +3,10 @@ LATEX=pdflatex BIBTEX=bibtex GENERATED_MACROS_TEX=generated_macros.tex +HEVEA_DIR=hevea +MATHJAX_CONFIG_JS=HTML/ASL-mathjax-config.js +HTML_STYLESHEET=$(HEVEA_DIR)/asl-html.css +HEVEA_HTML_INPUTS=book.hva mathjaxauto.hva $(HEVEA_DIR)/mathjax_config.hva macros.hva ASLReference.tex all: ASLReference.pdf @@ -21,12 +25,22 @@ ASLReference.pdf: generated_spec *.tex *.bib fi python3 doclint.py --console_macros --aslref $(ASLREF) -html: generated_spec *.tex *.bib *.hva +html: generated_spec *.tex *.bib *.hva $(HEVEA_DIR)/*.hva $(HEVEA_DIR)/generate_mathjax_config.py $(HTML_STYLESHEET) mkdir -p HTML - hevea -fix0 -O -o HTML/ASL.html book.hva macros.hva ASLReference.tex + cp $(HTML_STYLESHEET) HTML/asl-html.css + @# The first run is expected to generate warnings because bibhva + @# and the second hevea pass have not run, so we silence them via -s. + @# MathJax mode intentionally omits -O: Esponja does not understand the raw + @# TeX fragments that HeVeA leaves for MathJax to typeset in the browser. + hevea -fix0 -s -o HTML/ASL.html $(HEVEA_HTML_INPUTS) bibhva HTML/ASL - hevea -fix -O -o HTML/ASL.html book.hva macros.hva ASLReference.tex + @# bibhva makes citations available after the first pass; run one more + @# silent pass so the final unsilenced pass starts from stable references. + hevea -fix0 -s -o HTML/ASL.html $(HEVEA_HTML_INPUTS) + hevea -fix -o HTML/ASL.html $(HEVEA_HTML_INPUTS) + python3 $(HEVEA_DIR)/generate_mathjax_config.py $(MATHJAX_CONFIG_JS) HTML/ASL.html cd HTML && hacha ASL.html + python3 $(HEVEA_DIR)/generate_mathjax_config.py $(MATHJAX_CONFIG_JS) HTML/ASL[0-9][0-9][0-9].html generated_spec: asl.spec dune exec -- aslspec asl.spec --render; diff --git a/asllib/doc/StandardLibrary.tex b/asllib/doc/StandardLibrary.tex index 575b65c6f1..e13dcbdb06 100644 --- a/asllib/doc/StandardLibrary.tex +++ b/asllib/doc/StandardLibrary.tex @@ -2,7 +2,7 @@ \chapter{Standard Library\label{chap:StandardLibrary}} In addition to the operations, ASL provides some standard subprograms. The standard subprograms are available from the following address: -\url{https://github.com/herd/herdtools7/blob/\VERSION/asllib/libdir/stdlib.asl}. +\href{https://github.com/herd/herdtools7/blob/\VERSION/asllib/libdir/stdlib.asl}{\texttt{https://github.com/herd/herdtools7/blob/\VERSION/asllib/libdir/stdlib.asl}}. % The standard subprograms given there provide one way of implementing them. ASL implementations can implement the subprograms in any way that provides equivalent behaviour. diff --git a/asllib/doc/hevea/README.md b/asllib/doc/hevea/README.md new file mode 100644 index 0000000000..b50a649cfe --- /dev/null +++ b/asllib/doc/hevea/README.md @@ -0,0 +1,234 @@ +# ASL HTML HeVeA Support + +This directory contains the source-controlled support files for the ASL Reference HTML build. Generated files are written under `asllib/doc/HTML/` and +should not be edited by hand. + +Run the build from `asllib/doc`: + +```sh +make html +``` + +## Build Flow + +The `html` Makefile target: + +1. Generates `generated_macros.tex` from `asl.spec`. +2. Runs HeVeA on `ASLReference.tex` with: + - `book.hva` + - `mathjaxauto.hva` + - `hevea/mathjax_config.hva` + - `macros.hva` +3. Runs `bibhva` and additional HeVeA passes so citations and cross-references + settle. +4. Runs `hevea/generate_mathjax_config.py` on the unsplit `HTML/ASL.html`. + This prepares the MathJax source in that file and writes + `HTML/ASL-mathjax-config.js`. +5. Runs `hacha` to split `HTML/ASL.html` into chapter pages. +6. Runs `generate_mathjax_config.py` again on the split `HTML/ASLNNN.html` + pages. This updates the generated MathJax configuration with the final + split-page anchor map and prepares MathJax source in each split page. + +The first HeVeA passes use `-s` because citations and references are expected +to be incomplete until `bibhva` and the later HeVeA pass have run. The final +HeVeA pass is not silenced. + +The HTML build intentionally omits HeVeA's `-O` optimization flag. MathJax mode +leaves raw TeX fragments for the browser to typeset, and the optimizer does not +understand those fragments reliably. + +## Files + +### `mathjax_config.hva` + +Overrides HeVeA's default MathJax hook. + +HeVeA's built-in `mathjax.hva` loads an older MathJax setup directly. This file instead injects: +- `asl-html.css`, the ASL-specific stylesheet. +- `ASL-mathjax-config.js`, generated by `generate_mathjax_config.py`. +- MathJax from jsDelivr, pinned to an exact version and protected with Subresource Integrity (SRI). + +Keep this file small. Most ASL-specific behavior belongs in the generated MathJax config or in the stylesheet. + +#### MathJax Loading And Security + +The MathJax script is loaded from jsDelivr as: + +```html +https://cdn.jsdelivr.net/npm/mathjax@4.0.0/tex-chtml.js +``` + +The URL intentionally pins the exact `4.0.0` release instead of using a rolling +selector such as `mathjax@4`. A rolling selector is convenient, but the browser +may receive different JavaScript when MathJax publishes a new 4.x release. + +The script tag also includes an SRI hash and `crossorigin="anonymous"`. SRI +means the browser verifies the fetched script against the expected SHA-384 +digest and refuses to execute it if the CDN serves different content. + +This is the safest lightweight option for this build: + +- It avoids mutable CDN content by pinning the exact MathJax release. +- It detects CDN tampering or unexpected content changes via SRI. +- It avoids vendoring a large third-party MathJax distribution into the source + tree. + +Vendoring MathJax locally would remove the runtime CDN dependency entirely, but +would add a substantial third-party asset tree to the repository. If this +project later needs fully offline or CDN-free HTML, vendor the complete MathJax +distribution and update `mathjax_config.hva` to load it from `HTML/` or another +local path. + +When upgrading MathJax: + +1. Change the exact version in `mathjax_config.hva`. +2. Recompute the SRI hash for the new `tex-chtml.js`. +3. Update the `integrity` attribute. +4. Rebuild with `make html`. +5. Inspect representative formula-heavy pages. + +### `generate_mathjax_config.py` + +Prepares generated HTML pages for MathJax and writes +`HTML/ASL-mathjax-config.js`. + +The script does several related jobs: + +- Reads macro definitions from: + - `ASLmacros.tex` + - `variable_name_macros.tex` + - `generated_macros.tex` +- Converts simple LaTeX macro definitions into MathJax `configmacros` definitions. +- Resolves simple `\let` aliases, such as `\OldEmptyset`, before translating macro bodies. +- Provides manual MathJax definitions only for macros whose LaTeX definition is too complex, too PDF-specific, or visually unsuitable when translated directly. +- Wraps MathJax source fragments in temporary placeholder elements so the page can show animated grey formula placeholders while MathJax typesets. +- Moves `\hypertarget`, `\mathhypertarget`, and `\texthypertarget` out of + MathJax source and into static HTML anchors. MathJax should typeset formulas, + not create the document's structural anchors. +- Rewrites some TeX constructs before MathJax sees them, such as `\verb`, + `\textfunc`, and `\inferrule` labels. +- Builds a split-page anchor map after `hacha`, so generated MathJax hyperlinks + can point to the correct `ASLNNN.html#anchor` target. +- Writes `HTML/ASL-mathjax-fallbacks.txt`, a diagnostic report for macro + translations that should be reviewed. + +#### Hyperlinks In MathJax Macros + +MathJax macro bodies use `#` for macro arguments, which conflicts with URL +fragments such as `ASL011.html#type-ResultExpr`. The generator therefore writes +the temporary sentinel `__ASL_HASH__` inside generated `\href` targets and emits +JavaScript that repairs those links after MathJax creates real anchors. + +The repair code also runs on click, so links are corrected before navigation +even if MathJax updates the DOM late. + +#### Placeholder Rendering + +The generated HTML wraps formula source in: + +- `span.asl-mathjax-pending.asl-mathjax-inline` for inline formulas. +- `div.asl-mathjax-pending.asl-mathjax-display` for display formulas. + +`asl-html.css` renders those wrappers as animated grey placeholders. Once +MathJax finishes, `ASL-mathjax-config.js` removes the pending class and the real +formula becomes visible. A timeout fallback also removes the pending state if +MathJax fails to load. + +#### Diagnostics + +`HTML/ASL-mathjax-fallbacks.txt` contains: + +- `Unknown Macro Fallbacks`: macros used in MathJax source but not defined by + MathJax or the generated config. +- `Generic Operator Fallbacks`: argument-taking macros translated to generic + `\operatorname{name}(...)` forms. +- `Suspicious Zero-Argument Macro Translations`: zero-argument macros whose + source definition looks symbolic but whose generated expansion fell back to + the macro name. + +The last section is intended to catch issues like a macro whose PDF rendering is `\geq_{\text{pure}}` but whose HTML rendering would otherwise become the text `puritygeq`. + +#### Macro Translation Maintenance + +Do not add a macro to `MANUAL_MACROS` if the generator can derive the same +MathJax definition from the TeX source. The automatic translator handles the +common one-line cases: linked symbols, `\let` aliases, simple text/style +wrappers, simple superscript/subscript forms, and simple argument-taking +operators. + +Keep an entry in `MANUAL_MACROS` when the direct TeX expansion is not the HTML +rendering we want. Examples include: + +- Document-only helpers such as `\hva`, `\frontmatter`, and `\mainmatter`. +- MathJax structural shims such as `\inferrule`, `\hyperlink`, and + `\mathhypertarget`. +- Visual overrides where the PDF macro is technically valid TeX but looks poor + in MathJax, such as `\disjointunion`, `\parallelgraphs`, and empty-set + variants rendered with `\varnothing`. +- Multi-line macros or layout-sensitive macros whose `[H]`/`[V]` branches would + require real TeX interpretation. + +When a TeX macro changes, rebuild and inspect `HTML/ASL-mathjax-fallbacks.txt`. +If the generated definition is already correct, prefer improving the automatic +translator over adding another manual entry. + +### `asl-html.css` + +Additional styling for the generated ASL HTML pages. + +This stylesheet is copied to `HTML/asl-html.css` by `make html`. It layers on +top of the structural CSS emitted by HeVeA and should contain only ASL HTML +presentation rules, such as: + +- Page typography and spacing. +- Display-math overflow handling. +- MathJax placeholder styling and animation. +- Small ASL-specific visual rules, such as the red wrapped-line marker. + +Do not edit `HTML/asl-html.css` directly; edit this source file instead. + +## Generated Files + +The important generated files are: + +- `HTML/ASL.html`: the unsplit HeVeA output and `hacha` input. +- `HTML/ASLNNN.html`: split chapter/section pages. +- `HTML/index.html`: split HTML table of contents. +- `HTML/ASL-mathjax-config.js`: generated MathJax configuration and runtime + repair code. +- `HTML/ASL-mathjax-fallbacks.txt`: generated macro translation diagnostics. +- `HTML/asl-html.css`: copy of `hevea/asl-html.css`. + +These files are regenerated by `make html`. + +## Common Maintenance Tasks + +When a formula shows a macro name rather than the intended symbol: + +1. Check `HTML/ASL-mathjax-fallbacks.txt`. +2. If the macro appears in a fallback section, either improve the simple parser + in `generate_mathjax_config.py` or add a focused manual definition in + `MANUAL_MACROS`. +3. Rebuild with `make html`. +4. Inspect the affected `HTML/ASLNNN.html` page. + +When a MathJax hyperlink points to a bad URL: + +1. Check that the target has a real `id` in the split page. +2. Check the generated macro in `HTML/ASL-mathjax-config.js`. +3. If the URL contains `__ASL_HASH__` after clicking, review the link-repair + JavaScript in `generate_mathjax_config.py`. + +When raw LaTeX flashes before formulas render: + +1. Confirm the formula is wrapped in an `asl-mathjax-pending` element. +2. Check `asl-html.css` placeholder styles. +3. Check `finishAslMathJaxLoading()` in the generated config. + +## Constraints + +- Avoid adding new runtime or build dependencies unless they are really needed. +- Keep generated artifacts under `HTML/`; keep source changes in this directory + or the LaTeX sources. +- Prefer targeted manual MathJax definitions for hard PDF-specific macros over + broad parser changes that may affect unrelated output. diff --git a/asllib/doc/hevea/asl-html.css b/asllib/doc/hevea/asl-html.css new file mode 100644 index 0000000000..fd8109c827 --- /dev/null +++ b/asllib/doc/hevea/asl-html.css @@ -0,0 +1,259 @@ +/* + * Additional styling for the HeVeA HTML build of the ASL Reference. + * + * HeVeA emits a small structural stylesheet into each generated page. Keep + * these rules as a source-controlled layer on top of that output rather than + * editing files under HTML/, which are build artifacts. + */ + +:root { + color-scheme: light; + --asl-paper: #fffdf8; + --asl-background: #f3f1ea; + --asl-text: #1b1b18; + --asl-muted: #5d5b55; + --asl-rule: #d8d2c4; + --asl-code-background: #f6f3ea; +} + +html { + background: var(--asl-background); +} + +body { + box-sizing: border-box; + max-width: 72rem; + min-height: 100vh; + margin: 0 auto; + padding: 2.4rem 3.2rem 4rem; + background: var(--asl-paper); + color: var(--asl-text); + font-family: "Latin Modern Roman", "Computer Modern Serif", "STIX Two Text", + "Times New Roman", Times, serif; + font-size: 17px; + line-height: 1.5; +} + +p { + margin: 0.72rem 0; +} + +h1, +h2, +h3, +h4, +h5, +h6 { + color: var(--asl-text); + font-family: "Latin Modern Roman", "Computer Modern Serif", "STIX Two Text", + "Times New Roman", Times, serif; + font-weight: 700; + line-height: 1.18; +} + +h1.chapter { + margin-top: 2.4rem; + margin-bottom: 1.1rem; + padding-bottom: 0.35rem; + border-bottom: 1px solid var(--asl-rule); + font-size: 2rem; +} + +h2.section { + margin-top: 1.9rem; + margin-bottom: 0.75rem; + font-size: 1.55rem; +} + +h3.subsection { + margin-top: 1.45rem; + margin-bottom: 0.5rem; + font-size: 1.24rem; +} + +h4.subsubsection, +h5.paragraph { + margin-top: 1.1rem; + margin-bottom: 0.35rem; +} + +a { + color: #064f86; + text-decoration-thickness: 0.06em; + text-underline-offset: 0.12em; +} + +a:hover { + color: #083b63; +} + +ul, +ol, +dl { + margin-top: 0.65rem; + margin-bottom: 0.85rem; +} + +li { + margin: 0.25rem 0; +} + +blockquote, +.quote, +.quotation { + margin-left: 2rem; + margin-right: 2rem; + color: var(--asl-muted); +} + +pre, +.lstlisting, +.tt { + font-family: "Latin Modern Mono", "Computer Modern Typewriter", + ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; +} + +pre, +.lstlisting { + overflow-x: auto; + margin: 1rem 0; + padding: 0.85rem 1rem; + background: var(--asl-code-background); + border: 1px solid var(--asl-rule); + line-height: 1.35; +} + +table.title { + margin-top: 0.8rem; + margin-bottom: 2.4rem; +} + +.titlemain { + margin-bottom: 0.5rem; + font-size: 2.35rem; +} + +.titlerest { + color: var(--asl-muted); + font-size: 1.05rem; + font-weight: 400; +} + +.toc, +ul.toc { + padding-left: 0; + line-height: 1.35; +} + +.caption { + color: var(--asl-muted); + font-size: 0.95rem; +} + +.theorem { + margin: 1rem 0; +} + +.display, +.displaystack, +.vdisplay, +.vdisplaystack, +.equationcontainer, +mjx-container[display="true"] { + max-width: 100%; + overflow-x: auto; + overflow-y: hidden; +} + +mjx-container { + line-height: 1.2; +} + +mjx-container[display="true"] { + margin: 0.9rem 0; + padding: 0.1rem 0; +} + +.asl-mathjax-pending { + position: relative; + overflow: hidden; + color: transparent; + background: #e9e5dc; + background-image: linear-gradient( + 90deg, + #e9e5dc 0%, + #f8f6ef 45%, + #e9e5dc 90% + ); + background-size: 220% 100%; + animation: asl-mathjax-placeholder 1.2s ease-in-out infinite; +} + +.asl-mathjax-pending.asl-mathjax-inline { + display: inline-block; + width: var(--asl-mathjax-placeholder-width, 4em); + max-width: 18em; + height: 0.95em; + border-radius: 3px; + vertical-align: -0.12em; +} + +.asl-mathjax-pending.asl-mathjax-display { + display: block; + height: var(--asl-mathjax-placeholder-height, 3rem); + margin: 0.9rem 0; + border-radius: 4px; +} + +@keyframes asl-mathjax-placeholder { + from { + background-position: 100% 0; + } + + to { + background-position: -100% 0; + } +} + +@media (prefers-reduced-motion: reduce) { + .asl-mathjax-pending { + animation: none; + } +} + +.asl-wrappedline { + color: #c00000; +} + +.mprow { + border-spacing: 1.35rem 0.65rem; +} + +.mprcell { + padding: 0.1rem 0.25rem; + vertical-align: middle; +} + +hr.floatrule, +.footnoterule { + background-color: var(--asl-rule); +} + +@media (max-width: 720px) { + body { + padding: 1.2rem 1rem 2.5rem; + font-size: 16px; + } + + h1.chapter { + font-size: 1.7rem; + } + + h2.section { + font-size: 1.35rem; + } + + .titlemain { + font-size: 1.9rem; + } +} diff --git a/asllib/doc/hevea/generate_mathjax_config.py b/asllib/doc/hevea/generate_mathjax_config.py new file mode 100644 index 0000000000..23f4734ac1 --- /dev/null +++ b/asllib/doc/hevea/generate_mathjax_config.py @@ -0,0 +1,1047 @@ +#!/usr/bin/env python3 +"""Prepare ASL Reference MathJax HTML source and generate the MathJax configuration.""" + +from __future__ import annotations + +import json +import html +import re +import sys +from collections import Counter +from pathlib import Path + + +ROOT = Path(__file__).resolve().parent.parent +SOURCES = [ + ROOT / "ASLmacros.tex", + ROOT / "variable_name_macros.tex", + ROOT / "generated_macros.tex", +] + +MATH_CHUNK_RES = [ + re.compile(r"\\\((.*?)\\\)", re.DOTALL), + re.compile(r"\\\[(.*?)\\\]", re.DOTALL), + re.compile( + r"\\begin\{(?Pdisplaymath|math|equation\*?|align\*?|alignat\*?|eqnarray\*?|gather\*?|multline\*?)\}" + r".*?" + r"\\end\{(?P=env)\}", + re.DOTALL, + ), +] + +TARGET_ONE_ARG_RE = re.compile(r"\\(?:mathhypertarget|texthypertarget)\{([^{}]+)\}") +TARGET_TWO_ARG_RE = re.compile(r"\\hypertarget\{([^{}]+)\}\{([^{}]*)\}") +EXISTING_ID_RE = re.compile(r"\bid=(['\"])(.*?)\1") +WAVY_HELPER_RE = re.compile(r"\\my@wavy\{([^{}]*)\}") +VERB_RE = re.compile(r"\\verb(.)(.*?)\1") +TEXTFUNC_RE = re.compile(r"\\textfunc\{([^{}]*)\}") +STARRED_INFERRULE_RE = re.compile(r"\\inferrule\*") +INFERRULE_OPTION_RE = re.compile(r"\\inferrule\[([^\]]*)\]") +EMPTY_INFERRULE_PREMISE_RE = re.compile(r"(\\inferrule(?:\[[^\]]*\])?)\{\}") +SIMPLE_RULE_LABEL_RE = re.compile(r"(?:[A-Za-z0-9.]+|\\_)+\Z") +ANCHOR_ID_RE = re.compile(r"<[^>]+\bid=(['\"])(.*?)\1") +SOURCE_HYPERLINK_RE = re.compile(r"\\hyperlink\{([^{}]+)\}") +HREF_FRAGMENT_SENTINEL = "__ASL_HASH__" +LET_RE = re.compile(r"\\let\\(?P[A-Za-z@]+)\\(?P[A-Za-z@]+)") +UNSAFE_AUTO_TRANSLATION_RE = re.compile( + r"\\(?:hyperlink|ifthenelse|mathchoice|mathaccent|color|Hy@raisedlink)\b" +) + +MATHJAX_BUILTINS = { + "Big", + "Bigg", + "Biggl", + "Bigl", + "Bigm", + "Bigr", + "Delta", + "Gamma", + "Lambda", + "Large", + "Leftrightarrow", + "Longrightarrow", + "Rightarrow", + "Sigma", + "Theta", + "Vert", + "alpha", + "and", + "approx", + "array", + "backslash", + "begin", + "beta", + "big", + "bigg", + "bigl", + "bigr", + "cap", + "c", + "cdot", + "colon", + "color", + "cup", + "dfrac", + "displaystyle", + "dots", + "ell", + "ellipsis", + "emph", + "end", + "enspace", + "emptyset", + "epsilon", + "equiv", + "exists", + "forall", + "frac", + "gamma", + "ge", + "geq", + "gt", + "hbox", + "hline", + "href", + "implies", + "in", + "infty", + "iota", + "l", + "label", + "lambda", + "land", + "large", + "ldots", + "le", + "left", + "leftrightarrow", + "leq", + "lnot", + "Longleftarrow", + "Longleftrightarrow", + "longleftarrow", + "longleftrightarrow", + "longmapsto", + "longrightarrow", + "lor", + "lt", + "mapsto", + "mathbb", + "mathbin", + "mathcal", + "mathbf", + "mathit", + "mathop", + "mathrm", + "mathsf", + "mathtt", + "mbox", + "medspace", + "mid", + "mod", + "ne", + "neg", + "neq", + "nonumber", + "not", + "operatorname", + "or", + "otimes", + "overbrace", + "overbracket", + "overline", + "overset", + "phantom", + "pi", + "prime", + "providecommand", + "qquad", + "quad", + "r", + "ref", + "renewcommand", + "rightarrow", + "rightharpoonup", + "right", + "scriptstyle", + "scriptscriptstyle", + "setminus", + "sigma", + "sim", + "small", + "square", + "stackrel", + "subset", + "subseteq", + "supset", + "supseteq", + "tag", + "tau", + "text", + "textbackslash", + "textbf", + "textit", + "textrm", + "textsc", + "textsf", + "textstyle", + "texttt", + "theta", + "thickspace", + "thinspace", + "to", + "triangleq", + "times", + "underbrace", + "underbracket", + "underline", + "underset", + "uplus", + "varepsilon", + "vert", + "vdots", + "vphantom", + "wedge", + "xrightarrow", + "xleftarrow", +} + + +def mj_string(value: str) -> str: + return json.dumps(value, ensure_ascii=False) + + +def macro_value(value: str | list[object]) -> str: + if isinstance(value, str): + return mj_string(value) + return json.dumps(value, ensure_ascii=False) + + +def collect_anchor_map(paths: list[Path]) -> dict[str, str]: + split_pages = [path for path in paths if re.fullmatch(r"ASL\d+\.html", path.name)] + if not split_pages: + return {} + + anchors: dict[str, str] = {} + for path in split_pages: + if not path.exists(): + continue + for match in ANCHOR_ID_RE.finditer(path.read_text()): + anchors.setdefault(html.unescape(match.group(2)), path.name) + return anchors + + +def href_target(target: str, anchor_map: dict[str, str]) -> str: + # MathJax macro bodies use # for arguments. Keep URL fragments out of the + # macro body and repair the sentinel after MathJax has created real anchors. + if target.startswith(("http://", "https://", "mailto:", "#")): + return target.replace("#", HREF_FRAGMENT_SENTINEL) + if target in anchor_map: + return f"{anchor_map[target]}{HREF_FRAGMENT_SENTINEL}{target}" + return f"{HREF_FRAGMENT_SENTINEL}{target}" + + +def linked_macro_value( + value: str | list[object], + target: str, + anchor_map: dict[str, str], +) -> str | list[object]: + href = href_target(target, anchor_map) + if isinstance(value, str): + return rf"\href{{{href}}}{{{value}}}" + + linked = list(value) + linked[0] = rf"\href{{{href}}}{{{linked[0]}}}" + return linked + + +def mathjax_link_repair_script() -> str: + return r""" +function repairAslHref(href) { + return href + .replace(/__ASL_HASH__/g, '#') + .replace(/\.html\/+#/g, '.html#') + .replace(/\.html##/g, '.html#'); +} + +function repairAslMathJaxLink(link) { + const href = link.getAttribute('href'); + if (!href) { + return; + } + const repaired = repairAslHref(href); + if (repaired !== href) { + link.setAttribute('href', repaired); + } +} + +function repairAslMathJaxLinks() { + for (const link of document.querySelectorAll('a[href]')) { + repairAslMathJaxLink(link); + } +} + +function finishAslMathJaxLoading() { + for (const placeholder of document.querySelectorAll('.asl-mathjax-pending')) { + placeholder.classList.remove('asl-mathjax-pending'); + placeholder.removeAttribute('aria-busy'); + } +} + +document.addEventListener('click', (event) => { + const target = event.target && event.target.nodeType === 1 + ? event.target + : event.target && event.target.parentElement; + const link = target && target.closest('a[href]'); + if (link) { + repairAslMathJaxLink(link); + } +}, true); + +document.addEventListener('DOMContentLoaded', repairAslMathJaxLinks); +window.addEventListener('load', repairAslMathJaxLinks); +setTimeout(repairAslMathJaxLinks, 0); +setTimeout(repairAslMathJaxLinks, 100); +setTimeout(repairAslMathJaxLinks, 500); + +new MutationObserver(repairAslMathJaxLinks).observe(document.documentElement, { + childList: true, + subtree: true, + attributes: true, + attributeFilter: ['href'] +}); + +setTimeout(finishAslMathJaxLoading, 15000); +""" + + +def prepare_html_inputs(paths: list[Path]) -> None: + for path in paths: + if not path.exists(): + continue + path.write_text(rewrite_mathjax_source(path.read_text())) + + +def already_wrapped_math_chunk(text: str, start: int) -> bool: + prefix = text[max(0, start - 240) : start] + return bool( + re.search( + r'<(?:span|div)\s+class="asl-mathjax-pending asl-mathjax-(?:inline|display)"' + r'\s+aria-busy="true"\s+style="[^"]*">\s*\Z', + prefix, + ) + ) + + +def mathjax_placeholder(chunk: str) -> str: + display = chunk.startswith((r"\[", r"\begin")) + text_length = len(chunk) + line_count = chunk.count("\n") + 1 + + if display: + height = min(12.0, max(2.6, line_count * 0.9 + text_length / 420.0)) + return ( + '
' + f"{chunk}
" + ) + + width = min(18.0, max(2.0, text_length / 7.0)) + return ( + '' + f"{chunk}" + ) + + +def rewrite_mathjax_source(text: str) -> str: + seen = {match.group(2) for match in EXISTING_ID_RE.finditer(text)} + + def rewrite_chunk(match: re.Match[str]) -> str: + chunk = match.group(0) + already_wrapped = already_wrapped_math_chunk(text, match.start()) + ids: list[str] = [] + + def drop_one_arg(target: re.Match[str]) -> str: + ids.append(target.group(1)) + return "" + + def drop_two_arg(target: re.Match[str]) -> str: + ids.append(target.group(1)) + return target.group(2) + + chunk = TARGET_ONE_ARG_RE.sub(drop_one_arg, chunk) + chunk = TARGET_TWO_ARG_RE.sub(drop_two_arg, chunk) + chunk = WAVY_HELPER_RE.sub(r"\1", chunk) + chunk = VERB_RE.sub(rewrite_verb, chunk) + chunk = TEXTFUNC_RE.sub(rewrite_textfunc, chunk) + chunk = STARRED_INFERRULE_RE.sub(r"\\inferrule", chunk) + chunk = INFERRULE_OPTION_RE.sub(rewrite_inferrule_option, chunk) + chunk = EMPTY_INFERRULE_PREMISE_RE.sub(r"\1{\\vphantom{x}}", chunk) + + anchors = [] + for target_id in ids: + if target_id in seen: + continue + seen.add(target_id) + escaped_id = html.escape(target_id, quote=True) + anchors.append(f'') + + if not already_wrapped: + chunk = mathjax_placeholder(chunk) + + return "".join(anchors) + chunk + + for math_chunk_re in MATH_CHUNK_RES: + text = math_chunk_re.sub(rewrite_chunk, text) + return text + + +def rewrite_verb(match: re.Match[str]) -> str: + escaped = ( + match.group(2) + .replace("\\", r"\backslash ") + .replace("{", r"\{") + .replace("}", r"\}") + .replace("_", r"\_") + ) + return rf"\mathtt{{\text{{{escaped}}}}}" + + +def rewrite_textfunc(match: re.Match[str]) -> str: + label = match.group(1).replace(r"\_", "_").replace("_", r"\_") + return rf"\textfunc{{{label}}}" + + +def rewrite_inferrule_option(match: re.Match[str]) -> str: + # MathJax cannot uppercase rule labels or interpret mathpartir's + # right=... option, so normalize those before the macro expansion step. + label = match.group(1).strip() + if not label or label.startswith("right="): + return r"\inferrule[]" + + if not SIMPLE_RULE_LABEL_RE.fullmatch(label): + return match.group(0) + + display_label = label.replace(r"\_", "_").upper().replace("_", r"\_") + return rf"\inferrule[{display_label}]" + + +def tex_name(text: str) -> str: + return text.replace("_", r"\_") + + +def text_operator(name: str) -> str: + return rf"\mathop{{\text{{{name}}}}}" + + +def balanced_braces(text: str) -> bool: + depth = 0 + escaped = False + for char in text: + if escaped: + escaped = False + continue + if char == "\\": + escaped = True + continue + if char == "{": + depth += 1 + elif char == "}": + depth -= 1 + if depth < 0: + return False + return depth == 0 + + +def strip_outer_braces(text: str) -> str: + text = text.strip() + while text.startswith("{") and text.endswith("}") and balanced_braces(text[1:-1]): + text = text[1:-1].strip() + return text + + +def braced_arg(text: str, start: int) -> tuple[str, int] | None: + if start >= len(text) or text[start] != "{": + return None + + depth = 0 + escaped = False + for index in range(start, len(text)): + char = text[index] + if escaped: + escaped = False + continue + if char == "\\": + escaped = True + continue + if char == "{": + depth += 1 + elif char == "}": + depth -= 1 + if depth == 0: + return text[start + 1 : index], index + 1 + return None + + +def strip_full_hyperlink(text: str) -> str | None: + if not text.startswith(r"\hyperlink"): + return None + + target = braced_arg(text, len(r"\hyperlink")) + if target is None: + return None + body = braced_arg(text, target[1]) + if body is None or body[1] != len(text): + return None + return body[0].strip() + + +def strip_hyperlink_commands(text: str) -> str: + result: list[str] = [] + index = 0 + while index < len(text): + if text.startswith(r"\hyperlink", index): + target = braced_arg(text, index + len(r"\hyperlink")) + if target is not None: + body = braced_arg(text, target[1]) + if body is not None: + result.append(body[0]) + index = body[1] + continue + result.append(text[index]) + index += 1 + return "".join(result) + + +def collect_let_aliases() -> dict[str, str]: + aliases: dict[str, str] = {} + for source in SOURCES: + if not source.exists(): + continue + for line in source.read_text().splitlines(): + match = LET_RE.match(line.strip()) + if match: + aliases[match.group("alias")] = rf"\{match.group('target')}" + return aliases + + +def resolve_let_aliases(body: str, aliases: dict[str, str]) -> str: + for alias, target in sorted(aliases.items(), key=lambda item: len(item[0]), reverse=True): + body = re.sub(rf"\\{re.escape(alias)}(?![A-Za-z@])", lambda _match: target, body) + return body + + +def normalize_text_wrappers(body: str) -> str: + wrappers = { + "textsc": r"\mathrm", + "textsf": r"\mathsf", + "textit": r"\mathit", + "texttt": r"\mathtt", + "textbf": r"\mathbf", + "terminal": r"\mathtt", + "nonterminal": r"\mathtt", + } + for source, target in wrappers.items(): + body = re.sub( + rf"\\{source}\{{([^{{}}]+)\}}", + lambda match, target=target: rf"{target}{{{match.group(1)}}}", + body, + ) + body = re.sub( + r"\\textfunc\{([^{}]+)\}", + lambda match: text_operator(match.group(1)), + body, + ) + return body.replace(r"\xlongrightarrow", r"\xrightarrow") + + +def normalize_argument_braces(body: str) -> str: + body = re.sub(r"\{\{(#[0-9]+)\}\}", r"{\1}", body) + body = re.sub(r"(?<=[(\[,])\{(#[0-9]+)\}", r"\1", body) + body = re.sub(r"\{(#[0-9]+)\}(?=[)\],])", r"\1", body) + body = re.sub(r"\{(#[0-9]+)\}(?=\\right)", r"\1", body) + body = re.sub(r"\s+", " ", body) + return body.strip() + + +def auto_math_body(body: str, aliases: dict[str, str]) -> str | None: + body = strip_outer_braces(body) + while True: + linked_body = strip_full_hyperlink(body) + if linked_body is None: + break + body = strip_outer_braces(linked_body) + + body = strip_hyperlink_commands(body) + body = normalize_text_wrappers(resolve_let_aliases(body, aliases)) + body = normalize_argument_braces(body) + if not body or UNSAFE_AUTO_TRANSLATION_RE.search(body) or not balanced_braces(body): + return None + return body + + +def auto_arg_body( + body: str, + arity: int, + optional: str | None, + aliases: dict[str, str], +) -> str | list[object] | None: + body = auto_math_body(body, aliases) + if body is None or re.search(r"#[0-9]+", body) is None: + return None + if optional is not None and "#1" in body: + return None + if optional is None: + return [body, arity] + return [body, arity, optional] + + +def generic_macro(name: str, arity: int, optional: str | None) -> str | list[object]: + if arity == 0: + return rf"\mathit{{{tex_name(name)}}}" + + # Most optional arguments in ASL math macros are layout selectors such as + # [H] or [V]. Generic fallbacks should consume them so MathJax does not + # print the layout selector as a semantic argument. + first_mandatory_arg = 2 if optional is not None else 1 + args = ",".join(f"#{i}" for i in range(first_mandatory_arg, arity + 1)) + template = rf"\operatorname{{{tex_name(name)}}}\left({args}\right)" + if optional is None: + return [template, arity] + return [template, arity, optional] + + +def fallback_macro(name: str) -> str: + if name.isupper(): + return rf"\mathrm{{{tex_name(name)}}}" + return rf"\mathit{{{tex_name(name)}}}" + + +def is_fallback_macro(name: str, value: str | list[object]) -> bool: + return value == fallback_macro(name) + + +def is_generic_macro(name: str, value: str | list[object]) -> bool: + if isinstance(value, str): + return False + return bool(value) and value[0] == generic_macro(name, int(value[1]), value[2] if len(value) > 2 else None)[0] + + +def is_suspicious_zero_arg_body(body: str) -> bool: + body = body.strip() + if not body: + return False + return bool(re.search(r"\\|[_^{}<>]", body)) + + +def simple_no_arg_body(body: str, aliases: dict[str, str]) -> str | None: + body = body.strip() + link_match = re.fullmatch(r"\\hyperlink\{([^{}]*)\}\{(.+)\}", body) + if link_match: + body = link_match.group(2) + body = body.strip() + body = resolve_let_aliases(body, aliases) + + wrappers = { + "textsc": r"\mathrm", + "textsf": r"\mathsf", + "textit": r"\mathit", + "texttt": r"\mathtt", + "mathrm": r"\mathrm", + "mathsf": r"\mathsf", + "mathit": r"\mathit", + "mathtt": r"\mathtt", + "mathbb": r"\mathbb", + "mathcal": r"\mathcal", + "terminal": r"\mathtt", + "nonterminal": r"\mathtt", + } + for source, target in wrappers.items(): + match = re.fullmatch(rf"\\{source}\{{([^{{}}]+)\}}", body) + if match: + return rf"{target}{{{match.group(1)}}}" + + match = re.fullmatch(r"\\(?:mathrel|mathbin|mathop)\{(.+)\}", body) + if match: + return match.group(1) + + match = re.fullmatch(r"\\[A-Za-z]+", body) + if match: + return body + + match = re.fullmatch(r"\\textfunc\{([^{}]+)\}", body) + if match: + return text_operator(match.group(1)) + + match = re.fullmatch(r"\\verbatimterminal\{[^{}]+\}\{(.+)\}", body) + if match: + return rf"\mathtt{{\text{{{match.group(1)}}}}}" + + match = re.fullmatch(r"\{?([A-Za-z0-9_#\-]+)\}?", body) + if match: + return rf"\mathrm{{{tex_name(match.group(1))}}}" + + return auto_math_body(body, aliases) + + +def simple_arg_body( + body: str, + arity: int, + optional: str | None, + aliases: dict[str, str], +) -> str | list[object] | None: + body = body.strip() + body = strip_hyperlink_commands(body) + body = body.strip() + + match = re.fullmatch(r"\\(textsf|texttt|textit|textsc)\{([^{}]+)\}\(#1\)", body) + if arity == 1 and match: + wrapper = { + "textsf": r"\mathsf", + "texttt": r"\mathtt", + "textit": r"\mathit", + "textsc": r"\mathrm", + }[match.group(1)] + return [rf"{wrapper}{{{match.group(2)}}}\left(#1\right)", 1] + + match = re.fullmatch(r"\\([A-Za-z@]+)\\left\(#1\\right\)", body) + if arity == 1 and match: + return [rf"\{match.group(1)}\left(#1\right)", 1] + + return auto_arg_body(body, arity, optional, aliases) + + +COMMAND_RE = re.compile( + r"\\(?:(?:re)?newcommand|providecommand|providedcommand)(?:\\(?P[A-Za-z@]+)|\{\\(?P[A-Za-z@]+)\})" + r"(?:\[(?P\d+)\])?" + r"(?:\[(?P[^\]]*)\])?" + r"(?:\{(?P.*)\})?" +) + + +MacroSource = tuple[int, str, str | list[object], bool] + + +def collect_defined_macros() -> tuple[ + dict[str, str | list[object]], + dict[str, str], + dict[str, MacroSource], +]: + macros: dict[str, str | list[object]] = {} + macro_links: dict[str, str] = {} + macro_sources: dict[str, MacroSource] = {} + let_aliases = collect_let_aliases() + for source in SOURCES: + if not source.exists(): + continue + for line in source.read_text().splitlines(): + match = COMMAND_RE.match(line.strip()) + if not match: + continue + + name = match.group("name") or match.group("braced_name") + arity = int(match.group("arity") or 0) + optional = match.group("optional") + body = match.group("body") or "" + link_match = SOURCE_HYPERLINK_RE.search(body) + if link_match: + macro_links.setdefault(name, link_match.group(1)) + + value = ( + simple_no_arg_body(body, let_aliases) + if arity == 0 + else simple_arg_body(body, arity, optional, let_aliases) + ) + if name in MATHJAX_BUILTINS: + continue + used_generic_fallback = value is None + generated_value = value or generic_macro(name, arity, optional) + macros.setdefault(name, generated_value) + macro_sources.setdefault(name, (arity, body, generated_value, used_generic_fallback)) + return macros, macro_links, macro_sources + + +def collect_used_macros(paths: list[Path]) -> Counter[str]: + used: Counter[str] = Counter() + for path in paths: + if not path.exists(): + continue + text = path.read_text() + for math_chunk_re in MATH_CHUNK_RES: + for chunk in math_chunk_re.finditer(text): + used.update(re.findall(r"\\([A-Za-z@]+)\b", chunk.group(0))) + return used + + +def write_fallback_report( + path: Path, + macros: dict[str, str | list[object]], + macro_sources: dict[str, MacroSource], + used: Counter[str], + auto_fallbacks: set[str], +) -> None: + fallback_rows = [ + (used[name], name, macros[name]) + for name in auto_fallbacks + if used[name] and is_fallback_macro(name, macros[name]) + ] + generic_rows = [ + (used[name], name, macros[name]) + for name in macros + if used[name] and name not in MANUAL_MACROS and is_generic_macro(name, macros[name]) + ] + suspicious_zero_arg_rows = [ + (used[name], name, body, value) + for name, (arity, body, value, used_generic_fallback) in macro_sources.items() + if used[name] + and name not in MANUAL_MACROS + and arity == 0 + and used_generic_fallback + and is_suspicious_zero_arg_body(body) + ] + + def render_rows(title: str, rows: list[tuple[int, str, str | list[object]]]) -> list[str]: + lines = [title, "=" * len(title)] + for count, name, value in sorted(rows, reverse=True): + lines.append(f"{count:5d} {name}: {value!r}") + if len(lines) == 2: + lines.append("none") + lines.append("") + return lines + + def render_suspicious_zero_arg_rows( + title: str, + rows: list[tuple[int, str, str, str | list[object]]], + ) -> list[str]: + lines = [title, "=" * len(title)] + for count, name, body, value in sorted(rows, reverse=True): + lines.append(f"{count:5d} {name}:") + lines.append(f" source: {body!r}") + lines.append(f" generated: {value!r}") + if len(lines) == 2: + lines.append("none") + lines.append("") + return lines + + report_path = path.with_name("ASL-mathjax-fallbacks.txt") + report_path.write_text( + "\n".join( + render_rows("Unknown Macro Fallbacks", fallback_rows) + + render_rows("Generic Operator Fallbacks", generic_rows) + + render_suspicious_zero_arg_rows( + "Suspicious Zero-Argument Macro Translations", + suspicious_zero_arg_rows, + ) + ) + ) + + +MANUAL_MACROS: dict[str, str | list[object]] = { + # Keep these manual: target macros are moved into static HTML anchors before + # MathJax config generation. Any remaining target/link macros in MathJax + # source should not affect rendering. + "mathhypertarget": [r"", 1], + "texthypertarget": [r"", 1], + "hypertarget": [r"#2", 2], + "hyperlink": [r"#2", 2], + + # Keep these manual: they are HeVeA/document-structure helpers, not formula + # content. MathJax should silently consume them if any survive preprocessing. + "hva": r"", + "frontmatter": r"", + "mainmatter": r"", + "backmatter": r"", + + # Keep these manual: MathJax has its own text/style macros, but configmacros + # still needs definitions when these names appear in generated TeX fragments. + "texttt": [r"\mathtt{#1}", 1], + "textsf": [r"\mathsf{#1}", 1], + "textsc": [r"\mathrm{#1}", 1], + "textit": [r"\mathit{#1}", 1], + "textbf": [r"\mathbf{#1}", 1], + # Keep this manual: function names are literal text; using \operatorname + # with escaped underscores makes MathJax place underscores too low in the + # HTML output. + "textfunc": [r"\mathop{\text{#1}}", 1], + "terminal": [r"\mathtt{\text{#1}}", 1], + "nonterminal": [r"\mathtt{\text{#1}}", 1], + "verbatimterminal": [r"\mathtt{\text{#1}}", 2], + + # Keep these manual: the direct TeX definitions are legal but render worse in + # MathJax. These versions preserve labels, stable placeholder width, and the + # red wrapped-line marker used by the HTML stylesheet. + "overtext": [r"\overbracket{#1}^{\scriptstyle #2}", 2], + "overname": [r"\overbracket{#1}^{\scriptstyle #2}", 2], + "undertext": [r"\underbracket{#1}_{\scriptstyle #2}", 2], + "Ignore": r"\underline{\phantom{x}}", + "wrappedline": r"\class{asl-wrappedline}{\hookrightarrow}", + + # Keep these manual: the source definitions either depend on helper macros + # whose expansion is not useful to MathJax, or they need HTML-specific sizing + # and spacing to match the inspected rendering. + "aslrel": r"\mathbin{\Large\times}", + "typearrow": r"\xrightarrow{\mathsf{type}}", + "evalarrow": r"\xrightarrow{\mathsf{eval}}", + "parsesep": r"\;", + "terminateas": r"\;|\;", + # Keep this manual: mathpartir uses \and to separate premises or adjacent + # rules. MathJax does not provide that macro in this context, so render it as + # visual spacing. + "and": r"\qquad", + "opone": r"\mathbin{\mathtt{op1}}", + "optwo": r"\mathbin{\mathtt{op2}}", + "PIPE": r"\mid", + "bigtimes": r"\mathop{\Large\times}", + "disjointunion": r"\mathbin{\uplus}", + "parallelgraphs": [r"\mathop{\Large\|}#1", 1], + # Keep this manual: the source macro has horizontal/vertical branches. The + # HTML build intentionally consumes the layout selector and uses the compact + # horizontal form instead of trying to interpret TeX conditionals. + "ifthenelseop": [r"\mathbf{if}\;#2\;\mathbf{then}\;#3\;\mathbf{else}\;#4", 4, "V"], + # Keep these manual: MathJax's default \emptyset is visually too close to a + # slashed zero in these ASL constants; \varnothing matched the inspected HTML + # better and mirrors the previous hand-tuned rendering. + "emptyset": r"\varnothing", + "emptyfunc": r"\varnothing_{\lambda}", + "emptylist": r"[\;]", + "emptytenv": r"\varnothing_{\mathbb{SE}}", + "emptydenv": r"\varnothing_{\mathbb{DE}}", + "emptyenv": r"\varnothing_{\mathbb{E}}", + "empty": r"", + "emptygraph": r"\varnothing_{\mathsf{g}}", + + # Keep these manual: the automatic translator can recover many of these + # shapes, but the result is often a visually close expansion using helper + # macros or \mathop{\text{...}}. These definitions keep stable operator + # spelling, delimiter sizing, and optional-argument consumption. + "dom": r"\operatorname{dom}", + "graphof": [r"\operatorname{graph}\left(#1\right)", 1], + "environof": [r"\operatorname{environ}\left(#1\right)", 1], + "withgraph": [r"#2\left(\operatorname{graph}\mapsto #3\right)", 3, "H"], + "withenviron": [r"#2\left(\operatorname{environ}\mapsto #3\right)", 3, "H"], + "powfin": [r"\mathcal{P}_{\mathrm{fin}}\left(#1\right)", 1], + "rightarrowfin": r"\rightarrow_{\mathrm{fin}}", + "domop": [r"\operatorname{dom}\left(#1\right)", 1], + "cardinality": [r"\left|#1\right|", 1], + "rangeop": [r"\left[#2\ldots #3\right]", 3, "H"], + "mapupdate": [r"#2\left[#3\mapsto #4\right]", 4, "H"], + "mapapplyop": [r"#2\left(#3\right)", 3, "H"], + "makestructured": [r"#2\left(#3\right)", 3, "H"], + "listlen": [r"\left|#1\right|", 1], + "concatlist": [r"\operatorname{concat\_list}\left(#1\right)", 1], + "listcombine": [r"#2\mathbin{\otimes}#3", 3, "H"], + "listcombinethree": [r"#2\mathbin{\otimes_3}#3\mathbin{\otimes_3}#4", 4, "H"], + "listset": [r"\operatorname{list\_set}\left(#1\right)", 1], + "unionlistop": [r"\operatorname{union\_list}\left(#1\right)", 1], + "intersectionlistop": [r"\operatorname{intersection\_list}\left(#1\right)", 1], + "indicesop": [r"\operatorname{indices}\left(#1\right)", 1], + "bindings": [r"\operatorname{bindings}\left(#1\right)", 1], + "bindingstomap": [r"\operatorname{bindings\_to\_map}\left(#1\right)", 1], + "opnot": [r"\neg\left(#1\right)", 1], + "opnotvar": [r"\neg #1", 1], + "maybeemptylist": [r"\mathsf{list}^{*}\left(#1\right)", 1], + "parsenode": [r"\mathbb{PARSE}\left[#1\right]", 1], + "astlabelop": [r"\operatorname{ast\_label}\left(#1\right)", 1], + "astversion": [r"{#1}_{\mathtt{ast}}", 1], + "semanticsconfigurationterm": r"\text{semantics configuration}", + "Semanticsconfigurationterm": r"\text{Semantics configuration}", + "nvintop": [r"\mathtt{Int}\left(#1\right)", 1], + "nvboolop": [r"\mathtt{Bool}\left(#1\right)", 1], + "nvstringop": [r"\mathtt{String}\left(#1\right)", 1], + "nvbitvectorop": [r"\mathtt{Bitvector}\left(#1\right)", 1], + + # Inference rules. The HTML preparation phase normalizes simple rule labels + # to uppercase before MathJax sees them; render the optional label beside + # the rule instead of silently dropping it. + "inferrule": [ + r"\dfrac{\begin{array}{c}#2\end{array}}{#3}\quad{\scriptstyle\mathtt{#1}}", + 3, + "", + ], +} + + +def write_config(path: Path, html_inputs: list[Path]) -> None: + anchor_map = collect_anchor_map(html_inputs) + macros, macro_links, macro_sources = collect_defined_macros() + macros.update(MANUAL_MACROS) + for name, target in macro_links.items(): + if name in macros: + macros[name] = linked_macro_value(macros[name], target, anchor_map) + + used_macros = collect_used_macros(html_inputs) + auto_fallbacks = set() + for name in sorted(set(used_macros) - set(macros) - MATHJAX_BUILTINS): + macros[name] = fallback_macro(name) + auto_fallbacks.add(name) + + rendered = ",\n".join( + f" {json.dumps(name)}: {macro_value(value)}" + for name, value in sorted(macros.items()) + ) + + path.parent.mkdir(parents=True, exist_ok=True) + write_fallback_report(path, macros, macro_sources, used_macros, auto_fallbacks) + path.write_text( + """// AUTO-GENERATED by generate_mathjax_config.py. Do not edit by hand. +""" + + mathjax_link_repair_script() + + """ +window.MathJax = { + loader: { + load: [ + '[tex]/configmacros', + '[tex]/html', + '[tex]/mathtools', + '[tex]/extpfeil', + '[tex]/textmacros', + '[tex]/noerrors', + '[tex]/noundefined' + ] + }, + tex: { + packages: {'[+]': [ + 'configmacros', + 'html', + 'mathtools', + 'extpfeil', + 'textmacros', + 'noerrors', + 'noundefined' + ]}, + macros: { +""" + + rendered + + """ + } + }, + options: { + enableMenu: false + }, + startup: { + pageReady: () => MathJax.startup.defaultPageReady().then(() => { + repairAslMathJaxLinks(); + finishAslMathJaxLoading(); + }).catch((error) => { + finishAslMathJaxLoading(); + throw error; + }) + } +}; +""" + ) + + +def main(argv: list[str]) -> int: + if len(argv) < 2: + print("usage: generate_mathjax_config.py OUT.js [HTML ...]", file=sys.stderr) + return 2 + html_inputs = [Path(arg) for arg in argv[2:]] + prepare_html_inputs(html_inputs) + write_config(Path(argv[1]), html_inputs) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main(sys.argv)) diff --git a/asllib/doc/hevea/mathjax_config.hva b/asllib/doc/hevea/mathjax_config.hva new file mode 100644 index 0000000000..0ff1089e4e --- /dev/null +++ b/asllib/doc/hevea/mathjax_config.hva @@ -0,0 +1,12 @@ +% HeVeA's built-in mathjax.hva loads MathJax 2.7.1 directly from a CDN. +% Override that hook so the ASL HTML build can use a generated MathJax 4 +% configuration with ASL-specific macros and anchor handling. +% +% The MathJax URL is pinned to an exact release and protected with SRI. +% Avoid using the rolling "mathjax@4" selector: it can change over time. +% If this URL is upgraded, update the integrity hash at the same time. +\renewcommand{\jax@meta} +{\begin{rawhtml} + + +\end{rawhtml}}