Skip to content

HTML-FEATURES.md

Latest commit

 

History

History
140 lines (113 loc) · 7.37 KB

HTML-FEATURES.md

File metadata and controls

140 lines (113 loc) · 7.37 KB
Raw

Interactive HTML features (proven)

All three were validated end-to-end in a headless browser during the de-risking spike. The working assets live in pretext-template/. None require forking the PreTeXt core — they are a custom XSL that imports the core plus a client-side JS/CSS layer injected via the html.js.extra / html.css.extra params.

1. Formalization links — <lean>

A custom inline element:

<lean ref="MyProject.main_theorem">MyProject.main_theorem</lean>

xsl/custom-html.xsl renders it as a pill-styled link into the doc-gen4 find resolver (../lean/<project>/find/?pattern=<ref>#doc), with data-lean-ref as the hook the inline-knowl layer uses (a badge click opens the declaration's docs entry in place when the build-time registry has it).

Multiple independent formalizations (2026-07-12): <lean project="name"> selects the docs subset and the CSS class lean-proj-<name> — each project gets a distinct badge color, so readers can tell the formalizations apart at a glance. Project-less badges use the lean.docs.default.project XSL param. tex2ptx emits these from repeatable --lean-map PROJECT=PATH args (with --lean-badge-cap PROJECT=N for repos whose proofs decompose one statement into many declarations), and validators/lean_links.py checks each badge against its own project's tree via [inputs.formalizations.*] in paper.toml. Badges whose project has no built docs degrade to inert pills automatically (the registry sweep in detail-ui.js).

Follow-ups: add <lean> to the RELAX NG schema (else it fails validation once jing is installed); add a custom-latex.xsl template so it renders as a macro (e.g. \leanref) in the PDF instead of bare text.

2. Detail tiers — two carriers

  • PDF / default level: @component="detail-N" + a publication <version include="..."/> physically excludes higher tiers from the print build.
  • HTML interactive: a @detail-level="N" attribute is stamped onto the born-hidden knowl's <details> (via a one-template body-css-class override), and detail-ui.js mounts a global slider that sets details.open = (level <= threshold). Note: @component does not reach HTML, so the two carriers are intentionally separate.

3. Notation hovers without knowl underline

A \notn{key}{symbol} macro expands (via MathJax \class) to a ptxnotn-<key> class on the rendered symbol; detail-ui.js shows a small definition popup on hover/focus, positioned below the symbol so it never covers the equation. No knowl underline. Definitions come from a registry that the real tool should generate from the document's notation list, not hand-maintain.

Critical timing note: notation lives inside math, which MathJax typesets asynchronously after DOMContentLoaded. Wiring must wait for MathJax.startup.promise (see afterMathJax in detail-ui.js), or it finds zero nodes. The slider needs no such wait — its <details> are static HTML.

Integration follow-ups (from the spike)

  • Widget placement: appending to #ptx-masthead is not visible (fixed layout). Spike uses a fixed floating control; production should override the masthead template for a real slot.
  • Asset copying: html.*.extra only emit the tags; the JS/CSS files must be copied into the output dir. Needs a proper asset step.
  • custom-html.xsl imports the core via an absolute path; find the portable import path before this is truly reusable across machines/versions.

4. Far-notation affordance (\notnfar / .ptxfar)

Notation hovers are invisible until hover by design — but a symbol whose definition is many pages back deserves a visible cue. ingest/notation_far.py computes, in reading order, the word distance from each \notn{key} use to its defining site (<notation key> element or first use inside a <definition>), and rewrites uses beyond [notation] far_words (default 1500) to \notnfar{key}{sym} = \class{ptxfar}{\class{ptxnotn-key}{sym}}. Granularity is per symbol occurrence — two symbols in the same displayed equation can differ. CSS gives .ptxfar a default-visible dotted underline; the hover JS is unaffected (ptxfar deliberately does not share the ptxnotn- prefix).

Derived data: idempotent, recomputed after edits, never hand-written. Pre-definition uses are left unmarked (that is a notation_order error). Print safety: \providecommand{\class}[2]{#2} is injected into the LaTeX preamble (arxiv/print XSLs) so both macros degrade to their symbol in PDF.

Equation-range knowls

A range citation "(1.1)–(1.3)" is authored as two \eqrefs around an en dash, so PreTeXt gives knowls only for the endpoints. detail-ui's wireEquationRanges() detects the pattern (equation xref, en-dash text node, equation xref), checks that the display-math elements between the endpoints match the printed numbering, and wraps the whole range in one click target: clicking opens a single stacked panel showing EVERY equation in the range. Content is re-typeset from MathJax's stored TeX (getMathItemsWithin) — so middle equations need neither a knowl file (never cross-referenced) nor prior lazy typesetting — with the stored \tag{...} kept (the printed numbers) and \labels stripped (duplicate labels are MathJax errors). \notn wrappers survive, so notation hovers work inside the panel; .eqrange-knowl is in mathjax_macros.py's lazyAlwaysTypeset list. The panel's "view in context" uses the landingGo highlight (no :target flash).

Dark mode: key on the theme's class, not the media query

The PreTeXt modern theme drives dark entirely via a .dark-mode class on :root (readability-options.js sets it from prefers-color-scheme AND the user's manual toggle; theme.css has no media queries). Every paperforge style therefore keys on :root.dark-mode — a bare @media (prefers-color-scheme: dark) block disagrees with the manual toggle. paper-style.css holds the palette as CSS variables with a :root.dark-mode override block (values a step off the theme's dark body #23241f); detail-ui.css carries explicit .dark-mode counterparts for its literal values.

Accessibility of injected knowls

The click-to-open panels detail-ui.js injects (Lean declaration knowls, section-summary knowls) carry ARIA state: the toggle link tracks aria-expanded, and each panel is a role="region" with an aria-label naming its content ("Lean declaration MyProject.foo"; the division's label and title). New injected-panel features should follow the same pattern.

Homepage links and the ToC default

addHomeLinks() injects "← Project homepage" into the masthead and a "Return to the project homepage." line after the content footer — the paper is the one subpage PreTeXt generates, so the links cannot be authored. And the table of contents is visible by default on wide screens (owner request 2026-07-27): PreTeXt bakes the sidebar closed, build-web strips the hidden class, and a min-width: 1000px rule in paper-style.css shows it; the theme's toggle still closes it by re-adding .hidden.

Badges beyond theorem blocks (trust-base tables)

<lean> badges also render inside definition lists — the intro trust-base table (ingest/trust_table.py) lists each axiom interface with a badge on its Lean name, so .ptx-content dl .lean-link shares the pill styling and the ⚙ prefix. Any future structured-list surface that names declarations can reuse the same pattern: the badge selector, not the block type, is the contract.