diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2d4e8b25c..a1d50c9ac 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -191,6 +191,22 @@ jobs: browser-tests/test_redirect.py \ browser-tests/test_katex.py -v + - name: Run theme customization browser test + run: | + lake build theme-test-site + rm -rf _out/theme-test + lake exe theme-test-site --output _out/theme-test + uv run --project browser-tests --extra test pytest \ + browser-tests/theme-customization -v + + - name: Run theme picker browser test + run: | + # The picker test rebuilds the user's guide so it sees every shipped + # @[manual_theme] (Default, DefaultDark, ChromaticLight/Dark, BeaconLight/Dark) + # and can exercise switching between them. + uv run --project browser-tests --extra test pytest \ + browser-tests/theme-picker -v + - name: Build the VersoHtml site for browser tests run: | # The verso-html genre renders literate JSON into a standalone HTML site. diff --git a/.gitignore b/.gitignore index d09b011bd..cf07c1971 100644 --- a/.gitignore +++ b/.gitignore @@ -17,3 +17,8 @@ single.json *.html *.produced.out __pycache__ +main.toc +main.aux +main.log +main.out +main.pdf diff --git a/UsersGuideMain.lean b/UsersGuideMain.lean index c3f44a417..e4efe7150 100644 --- a/UsersGuideMain.lean +++ b/UsersGuideMain.lean @@ -7,6 +7,14 @@ open Verso.Genre.Manual def config : Config := { sourceLink := some "https://github.com/leanprover/verso", issueLink := some "https://github.com/leanprover/verso/issues" + -- The user's guide ships every theme as a live example, including ones with documented + -- accessibility trade-offs — most notably the canonical Solarized palette, whose token + -- colors are below WCAG AA's 4.5:1 contrast threshold for normal text by design. The + -- coverage and default-accessibility checks still fire (the default theme pair must be + -- accessible, and the registered set must offer an accessible choice on both + -- appearances), and per-theme warnings still surface the individual issues; the per-theme + -- warnings are silenced here to keep the build log readable. + warnPerThemeAccessibility := false } -def main := manualMain (%doc UsersGuide.Basic) +def main := manualMain (%doc UsersGuide.Basic) (config := { config with : RenderConfig }) diff --git a/browser-tests/theme-customization/__init__.py b/browser-tests/theme-customization/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/browser-tests/theme-customization/test_theme_customization.py b/browser-tests/theme-customization/test_theme_customization.py new file mode 100644 index 000000000..e3a4734eb --- /dev/null +++ b/browser-tests/theme-customization/test_theme_customization.py @@ -0,0 +1,301 @@ +""" +Browser test that pins a representative subset of themed CSS variables to their rendered DOM +values. The test currently exercises the four token color fields (keyword, const, var, fallback) +plus the error indicator border. Other themed fields are emitted to `verso-themes.css` but are +not all asserted here; expanding coverage is straightforward as more rendered features land in +the small test document. + +Workflow: + +1. Build the `theme-test-site` Lean exe, which renders a small Manual document with a + customized `CodeTheme` whose every color field holds a distinct sentinel value. +2. Serve the resulting `_out/theme-test/html-multi` directory. +3. For each themed element in the generated HTML, read its computed style and assert it + matches the sentinel hex value the Lean theme set for that field. + +If the rendered color drifts from the Lean theme value, the theme pipeline +(`CodeTheme.cssVariables` -> generated `verso-themes.css` -> `highlightingStyle` +`var(--verso-*)` lookups) is broken end-to-end. +""" + +import socket +import subprocess +import time +from pathlib import Path + +import pytest +from playwright.sync_api import sync_playwright + + +HERE = Path(__file__).parent +REPO_ROOT = HERE.parent.parent +SITE_DIR = REPO_ROOT / "_out" / "theme-test" / "html-multi" + + +def _hex_to_rgb(h: str) -> str: + h = h.lstrip("#") + if len(h) == 3: + h = "".join(c * 2 for c in h) + r, g, b = (int(h[i : i + 2], 16) for i in (0, 2, 4)) + return f"rgb({r}, {g}, {b})" + + +# Sentinel colors mirroring `src/tests/ThemeTestMain.lean`. +THEME = { + "background": "#000101", + "codeBlockBackground": "#000202", + "textColor": "#000303", + "codeColor": "#000404", + "selectedColor": "#000606", + "infoIndicatorColor": "#000808", + "warningIndicatorColor": "#000a0a", + "errorIndicatorColor": "#000c0c", + "hoverBackground": "#000d0d", + "constColor": "#001717", + "keywordColor": "#001818", + "varColor": "#001919", + # ManualTheme additions (chrome). + "headerBackground": "#001b1b", + "tocBackground": "#001c1c", + "linkColor": "#002020", + "tocTextColor": "#002222", + "borderColor": "#001d1d", + "mutedColor": "#001e1e", + "highlightColor": "#001f1f", +} + + +def _find_free_port() -> int: + with socket.socket(socket.AF_INET, socket.SOCK_STREAM) as s: + s.bind(("127.0.0.1", 0)) + return s.getsockname()[1] + + +@pytest.fixture(scope="module") +def built_site(): + """Rebuilds the customized-theme test site under `_out/theme-test`.""" + subprocess.check_call( + ["lake", "build", "theme-test-site"], + cwd=REPO_ROOT, + ) + if SITE_DIR.exists(): + # Wipe so a stale build can't pass a renamed/deleted assertion. + subprocess.check_call(["rm", "-rf", str(SITE_DIR.parent)], cwd=REPO_ROOT) + subprocess.check_call( + ["lake", "exe", "theme-test-site", "--output", "_out/theme-test"], + cwd=REPO_ROOT, + ) + assert SITE_DIR.exists(), f"Manual build did not produce {SITE_DIR}" + return SITE_DIR + + +@pytest.fixture(scope="module") +def server(built_site): + port = _find_free_port() + proc = subprocess.Popen( + ["python", "-m", "http.server", str(port), "--bind", "127.0.0.1"], + cwd=built_site, + stdout=subprocess.DEVNULL, + stderr=subprocess.DEVNULL, + ) + time.sleep(0.5) + try: + yield f"http://127.0.0.1:{port}" + finally: + proc.terminate() + proc.wait() + + +@pytest.fixture(scope="module") +def playwright_instance(): + with sync_playwright() as p: + yield p + + +@pytest.fixture(scope="module", params=["chromium", "firefox"]) +def page(request, playwright_instance, server): + browser = getattr(playwright_instance, request.param).launch() + page = browser.new_page() + page.goto(server + "/Code-samples/") + yield page + browser.close() + + +def _color(page, selector: str, prop: str = "color") -> str: + return page.evaluate( + "([sel, p]) => getComputedStyle(document.querySelector(sel)).getPropertyValue(p)", + [selector, prop], + ).strip() + + +def _expect(actual: str, hex_value: str, description: str) -> None: + expected = _hex_to_rgb(hex_value) + assert actual == expected, ( + f"{description}: expected {expected} ({hex_value}), got {actual}" + ) + + +def test_token_colors(page): + # The first `.keyword` in the only code block is `def`. + _expect( + _color(page, "code.hl.lean .keyword"), THEME["keywordColor"], "keyword color" + ) + # `.const` on `hello` (the function name) and `String` (the type). + _expect(_color(page, "code.hl.lean .const"), THEME["constColor"], "const color") + # `.var` on `name` (the parameter binding). + _expect(_color(page, "code.hl.lean .var"), THEME["varColor"], "var color") + # `.unknown` (operator-like tokens) falls back to `--verso-code-color`. + _expect( + _color(page, "code.hl.lean .unknown"), THEME["codeColor"], "fallback code color" + ) + + +def _goto_diagnostics(page, server): + page.goto(server + "/Diagnostics/") + + +def test_error_indicator(page, server): + _goto_diagnostics(page, server) + _expect( + _color(page, "pre.lean-output.error", "border-left-color"), + THEME["errorIndicatorColor"], + "lean-output.error indicator border", + ) + + +def test_page_background(page): + _expect( + _color(page, "body", "background-color"), THEME["background"], "body background" + ) + + +def test_body_text_color(page): + # `body` now sets `color: var(--verso-text-color)`. Inherited text in prose elements + # (paragraphs in `main`) should resolve to the theme's textColor rather than the + # browser-default black. + _expect(_color(page, "main p"), THEME["textColor"], "body prose color") + + +def test_header_background(page): + _expect( + _color(page, "header", "background-color"), + THEME["headerBackground"], + "header background", + ) + + +def test_header_title_color(page): + # `.header-title` previously hardcoded `color: black`; the theme's `textColor` is now what + # the rendered title actually uses, so a theme with textColor != black is readable on + # a non-white header background. + _expect( + _color(page, ".header-title"), + THEME["textColor"], + "header title color", + ) + + +def test_toc_background_and_link_color(page): + _expect( + _color(page, "#toc", "background-color"), + THEME["tocBackground"], + "toc background", + ) + # `#toc a` previously hardcoded `color: #333`; the theme's `tocTextColor` is now used, + # so a dark ToC background plus a light tocTextColor stays readable. + _expect( + _color(page, "#toc a"), + THEME["tocTextColor"], + "toc link color", + ) + + +def test_content_link_color(page, server): + # The doc has an `` content link inside `main`. The new + # `main a { color: var(--verso-link-color) }` rule should pick up the theme's linkColor. + page.goto(server + "/Code-samples/") + _expect( + _color(page, 'main a[href^="https://example.com"]'), + THEME["linkColor"], + "content link color", + ) + + +def _root_var(page, name: str) -> str: + """Resolves a CSS custom property at the document-root level to its computed `rgb(...)`.""" + return page.evaluate( + "(name) => {" + " const raw = getComputedStyle(document.documentElement).getPropertyValue(name).trim();" + " if (raw.startsWith('rgb')) return raw;" + " const probe = document.createElement('span');" + " probe.style.color = raw;" + " document.body.appendChild(probe);" + " const out = getComputedStyle(probe).color;" + " probe.remove();" + " return out;" + "}", + name, + ).strip() + + +def test_border_var(page): + # `borderColor` is the search-input border color (and other chrome borders); the search box + # is mounted by JS so the variable is the most direct verification that the theme value + # reaches the page. (The CSS rules in search-box.css / search-page.css use + # `var(--verso-border-color, gray)` so a missing variable would fall back to gray.) + _expect( + _root_var(page, "--verso-border-color"), THEME["borderColor"], "borderColor var" + ) + + +def test_prev_next_nav_color(page, server): + # The `.prev-next-buttons > *` rule previously hardcoded `color: black`. It now reads + # `var(--verso-text-color)` — section navigation is body-text colored, not link-colored, + # so it stays readable on any themed background without competing with content links. + # Both `:link` and `:visited` must land on text color; the visited-link rule for `main a` + # has higher specificity than `.prev-next-buttons > *` and would otherwise paint visited + # prev/next links in the visited-link color. + page.goto(server + "/Code-samples/") + # Force the prev page into the visited-link state by navigating to it once and back. + page.evaluate("history.replaceState({}, '', '/Diagnostics/')") + page.goto(server + "/Diagnostics/") + page.goto(server + "/Code-samples/") + colors = page.evaluate( + """() => { + const links = Array.from(document.querySelectorAll('.prev-next-buttons > a')); + return links.map(a => getComputedStyle(a).color); + }""" + ) + expected = _hex_to_rgb(THEME["textColor"]) + assert colors and all(c == expected for c in colors), ( + f"all prev/next links should be {expected}; got {colors}" + ) + + +def test_search_placeholder_muted(page, server): + # The quick-search placeholder previously hardcoded `#888` and the "more results" row `#777`. + # Both now route through `--verso-muted-color`. The search box itself is mounted by JS; + # waiting for the placeholder text confirms the rule reaches a real rendered element. + page.goto(server + "/Code-samples/") + placeholder = page.locator("#search-wrapper .cb_edit:empty").first + placeholder.wait_for(state="attached", timeout=10000) + color = page.evaluate( + "() => getComputedStyle(document.querySelector('#search-wrapper .cb_edit:empty')," + " '::before').getPropertyValue('color')" + ).strip() + _expect(color, THEME["mutedColor"], "search placeholder color") + + +def test_search_match_highlight(page, server): + # Full-page search results render each matched term inside an ``, whose background + # comes from `--verso-highlight-color` via `search-page.css`. Driving an actual search + # confirms a rendered match `` consumes the theme value (root variable existence is + # not enough; the CSS rule has to actually read it). + page.goto(server + "/search/?q=hello") + em = page.locator(".search-page-list li.search-result em").first + em.wait_for(state="attached", timeout=10000) + _expect( + _color(page, ".search-page-list li.search-result em", "background-color"), + THEME["highlightColor"], + "search-result match highlight", + ) diff --git a/browser-tests/theme-picker/__init__.py b/browser-tests/theme-picker/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/browser-tests/theme-picker/test_theme_picker.py b/browser-tests/theme-picker/test_theme_picker.py new file mode 100644 index 000000000..f10c0a38b --- /dev/null +++ b/browser-tests/theme-picker/test_theme_picker.py @@ -0,0 +1,663 @@ +""" +Browser tests for the theme picker (gear button + popover + dropdowns). + +Builds the user's guide (which ships multiple themes via @[manual_theme]) and exercises: + * gear placement in header-tools, left of the search box + * popover open/close, role + aria-* attributes, Escape returns focus to the gear + * focus trap inside the popover + * the Appearance radios (Light / Dark / Follow system) drive data-verso-theme and + data-verso-appearance, and persist across reloads via localStorage + * "Follow system" tracks matchMedia(prefers-color-scheme); Light/Dark lock the appearance + * the collapsible "Theme choices" section is expanded only when a non-default light or dark + theme is stored + * graceful degradation when localStorage throws (page still loads, default theme applied) +""" + +import socket +import subprocess +import time +from pathlib import Path + +import pytest +from playwright.sync_api import sync_playwright + + +HERE = Path(__file__).parent +REPO_ROOT = HERE.parent.parent +SITE_DIR = REPO_ROOT / "_out" / "usersguide" / "html-multi" + + +def _find_free_port() -> int: + with socket.socket(socket.AF_INET, socket.SOCK_STREAM) as s: + s.bind(("127.0.0.1", 0)) + return s.getsockname()[1] + + +@pytest.fixture(scope="module") +def built_site(): + subprocess.check_call( + ["lake", "build", "usersguide"], + cwd=REPO_ROOT, + ) + if SITE_DIR.parent.exists(): + subprocess.check_call(["rm", "-rf", str(SITE_DIR.parent)], cwd=REPO_ROOT) + subprocess.check_call( + [ + "lake", + "exe", + "usersguide", + "--output", + "_out/usersguide", + "--without-tex", + "--without-html-single", + "--with-html-multi", + ], + cwd=REPO_ROOT, + ) + assert SITE_DIR.exists(), f"Manual build did not produce {SITE_DIR}" + return SITE_DIR + + +@pytest.fixture(scope="module") +def server(built_site): + port = _find_free_port() + proc = subprocess.Popen( + ["python", "-m", "http.server", str(port), "--bind", "127.0.0.1"], + cwd=built_site, + stdout=subprocess.DEVNULL, + stderr=subprocess.DEVNULL, + ) + time.sleep(0.5) + try: + yield f"http://127.0.0.1:{port}" + finally: + proc.terminate() + proc.wait() + + +@pytest.fixture(scope="module") +def playwright_instance(): + with sync_playwright() as p: + yield p + + +@pytest.fixture(params=["chromium", "firefox"]) +def page(request, playwright_instance, server): + """Per-test page so localStorage / focus state don't leak between tests.""" + browser = getattr(playwright_instance, request.param).launch() + context = browser.new_context() + p = context.new_page() + p.goto(server + "/") + yield p + context.close() + browser.close() + + +def _picker_button(page): + return page.locator("#theme-picker-button") + + +def _dialog(page): + return page.locator("#theme-picker-dialog") + + +def _expand_choices(page): + """Open the collapsible Light/Dark "Theme choices" section if it isn't already open.""" + choices = page.locator("#theme-picker-choices") + if choices.count() and choices.get_attribute("open") is None: + page.locator("#theme-picker-choices > summary").click() + + +def _set_mode(page, mode): + """Select an Appearance radio button: 'light', 'dark', or 'auto'.""" + page.locator(f"#theme-picker-mode-{mode}").check() + + +def test_gear_height_and_centering_match_search(page): + """The gear glyph's ink height should be about 90% of the search input's outer height, + and the two centers should be aligned vertically. (The user asked for "90% as tall as + the search field and vertically centered with respect to the search field".)""" + page.set_viewport_size({"width": 1400, "height": 800}) + page.locator("#theme-picker-button").wait_for(state="visible", timeout=5000) + m = page.evaluate( + """() => { + const gear = document.querySelector('#theme-picker-button .theme-picker-gear'); + const input = document.querySelector('#search-wrapper .cb_edit'); + // The visible glyph rect, not the line-box, is what reads as "the gear's + // height" — `Range.getBoundingClientRect()` snaps to the rendered ink box. + const r = document.createRange(); + r.selectNodeContents(gear); + const ink = r.getBoundingClientRect(); + const ir = input.getBoundingClientRect(); + return { + ink_h: ink.height, + input_h: ir.height, + ink_mid: (ink.top + ink.bottom) / 2, + input_mid: (ir.top + ir.bottom) / 2, + }; + }""" + ) + ratio = m["ink_h"] / m["input_h"] + offset = abs(m["ink_mid"] - m["input_mid"]) + # The Unicode `⚙` glyph's visible cog is about 70-75% of its ink rect — i.e. an ink + # rect that matches the input optically reads smaller than the input. To get the gear + # to *look* like it matches the search field, the rendered ink rect needs to overshoot + # the input by ~15-25%. The acceptance band brackets that, with a little extra + # tolerance for cross-browser font metrics (Firefox renders the glyph metrics a couple + # of percent above Chromium at the same `font-size`). + assert 1.10 <= ratio <= 1.35, ( + f"gear glyph height {m['ink_h']:.2f}px is {ratio:.2%} of the search input height " + f"({m['input_h']:.2f}px); want ~115–125% so the optical cog matches the field" + ) + # Visual centering tolerance: one pixel is below the perceptual threshold for "off + # center" at standard zoom. + assert offset <= 1.0, ( + f"gear glyph center is {offset:.2f}px from the search input center; want <1px" + ) + + +def test_gear_in_header_tools_left_of_search(page): + btn = _picker_button(page) + btn.wait_for(state="attached", timeout=5000) + assert btn.is_visible() + # The gear sits inside `.header-tools` and that block is ordered before the search + # box by the `order: -1` rule in theme-picker.css. Verify the gear is geometrically + # to the left of the search box on a desktop viewport. + page.set_viewport_size({"width": 1200, "height": 800}) + gear_box = btn.bounding_box() + search = page.locator("#search-wrapper") + if search.count() > 0: + search_box = search.first.bounding_box() + if search_box is not None and gear_box is not None: + assert gear_box["x"] < search_box["x"], ( + f"gear at x={gear_box['x']}, search at x={search_box['x']}" + ) + + +def test_popover_open_close_aria(page): + btn = _picker_button(page) + btn.wait_for(state="attached", timeout=5000) + assert btn.get_attribute("aria-expanded") == "false" + btn.click() + d = _dialog(page) + d.wait_for(state="attached", timeout=5000) + assert btn.get_attribute("aria-expanded") == "true" + assert d.get_attribute("role") == "dialog" + assert d.get_attribute("aria-label") is not None + # Escape closes and returns focus to the gear. + page.keyboard.press("Escape") + page.wait_for_function( + "document.getElementById('theme-picker-button').getAttribute('aria-expanded') === 'false'" + ) + assert page.evaluate("document.activeElement.id") == "theme-picker-button" + + +def test_focus_trap(page): + btn = _picker_button(page) + btn.click() + dialog = _dialog(page) + dialog.wait_for(state="attached", timeout=5000) + # The focus trap pushes Tab from the last focusable back to the first; just check that + # repeated Tab presses keep focus within the dialog. + for _ in range(10): + page.keyboard.press("Tab") + in_dialog = page.evaluate( + "document.getElementById('theme-picker-dialog').contains(document.activeElement)" + ) + assert in_dialog, "focus escaped the dialog" + + +def test_appearance_radios_offer_light_dark_follow_system(page): + """The Appearance group offers exactly Light / Dark / Follow system radios, in that order.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + radios = page.locator("#theme-picker-mode input[type=radio]") + values = radios.evaluate_all("els => els.map(e => e.value)") + labels = page.locator("#theme-picker-mode .theme-picker-radio").all_text_contents() + assert values == ["light", "dark", "auto"], f"unexpected radio values {values!r}" + assert [t.strip() for t in labels] == ["Light", "Dark", "Follow system"], ( + f"unexpected radio labels {labels!r}" + ) + + +def test_first_visit_defaults_to_follow_system(page): + """A fresh visitor (no stored mode) sees the Appearance group on 'Follow system'.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + assert page.locator("#theme-picker-mode-auto").is_checked() + assert not page.locator("#theme-picker-mode-light").is_checked() + assert not page.locator("#theme-picker-mode-dark").is_checked() + + +def test_default_mode_exposed_and_drives_initial_radio(page): + """`window.versoThemes.defaultMode` is the author-configured starting mode (the user's guide + uses the default `followSystem`, encoded as `auto`), and the picker starts on it when nothing + is stored.""" + default_mode = page.evaluate("window.versoThemes.defaultMode") + assert default_mode == "auto", ( + f"expected exposed defaultMode 'auto', got {default_mode!r}" + ) + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + assert page.locator(f"#theme-picker-mode-{default_mode}").is_checked() + + +def test_light_mode_switching_persists(page, server): + """Selecting Light mode and a non-default light theme sets the data attributes and + survives a reload (the no-flash script reapplies it before paint).""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _set_mode(page, "light") + _expand_choices(page) + light = page.locator("#theme-picker-light") + current = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + chosen = None + for opt in light.locator("option").all(): + v = opt.get_attribute("value") + if v and v != current: + chosen = v + break + if chosen is None: + pytest.skip("not enough light themes registered to test switching") + light.select_option(value=chosen) + assert ( + page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + == chosen + ) + assert page.evaluate("localStorage.getItem('verso-theme-light')") == chosen + assert page.evaluate("localStorage.getItem('verso-theme-mode')") == "light" + # Reload: the no-flash script reads localStorage and applies the same theme before paint. + page.goto(server + "/") + page.wait_for_load_state("domcontentloaded") + assert ( + page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + == chosen + ) + + +def test_follow_system_tracks_media(page): + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _set_mode(page, "auto") + # Emulate dark, then light; the inline script's matchMedia listener should swap themes. + page.emulate_media(color_scheme="dark") + page.wait_for_timeout(50) + dark_id = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + dark_appearance = page.evaluate( + "document.documentElement.getAttribute('data-verso-appearance')" + ) + page.emulate_media(color_scheme="light") + page.wait_for_timeout(50) + light_id = page.evaluate( + "document.documentElement.getAttribute('data-verso-theme')" + ) + light_appearance = page.evaluate( + "document.documentElement.getAttribute('data-verso-appearance')" + ) + assert dark_id != light_id, ( + "Follow system should pick different themes for light vs dark" + ) + assert dark_appearance == "dark" and light_appearance == "light" + + +def test_locked_appearance_ignores_media(page): + """Light mode locks the appearance: a system media change must not override the theme.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _set_mode(page, "light") + chosen = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + page.emulate_media(color_scheme="dark") + page.wait_for_timeout(50) + assert ( + page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + == chosen + ) + assert ( + page.evaluate("document.documentElement.getAttribute('data-verso-appearance')") + == "light" + ) + page.emulate_media(color_scheme="light") + page.wait_for_timeout(50) + assert ( + page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + == chosen + ) + + +def test_auto_commit_applies_dropdown_value(page): + """In Follow-system mode under `prefers-color-scheme: light`, changing the light dropdown + should immediately apply the chosen light theme. The committed `data-verso-theme` must + match the dropdown's value, not whatever was previously painted.""" + page.emulate_media(color_scheme="light") + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _set_mode(page, "auto") + _expand_choices(page) + light = page.locator("#theme-picker-light") + current = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + chosen = None + for opt in light.locator("option").all(): + v = opt.get_attribute("value") + if v and v != current: + chosen = v + break + assert chosen is not None, "need at least two light themes to test commit" + light.select_option(value=chosen) + after = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + assert after == chosen, ( + f"auto-mode commit should apply dropdown value {chosen!r}, got {after!r}" + ) + + +def test_switching_themes_has_no_intermediate_state(page): + """Selecting a new theme in the dropdown must take `data-verso-theme` directly from the + old value to the new value. Any intermediate state — e.g. a transient default — would + cause a visible flash to an unrelated theme.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + # Light mode keeps the test deterministic: the active theme is exactly the light dropdown's + # value, so the test exercises "open the dialog, pick a different light theme, see only the + # new theme paint." + _set_mode(page, "light") + _expand_choices(page) + # Install a MutationObserver that logs every value `data-verso-theme` takes from this + # point on, so we can assert the sequence after the switch. + page.evaluate( + """() => { + window.__versoThemeStates = []; + const obs = new MutationObserver(records => { + for (const r of records) { + if (r.attributeName === 'data-verso-theme') { + window.__versoThemeStates.push( + document.documentElement.getAttribute('data-verso-theme') + ); + } + } + }); + obs.observe(document.documentElement, { attributes: true }); + window.__versoStopObserver = () => obs.disconnect(); + }""" + ) + light = page.locator("#theme-picker-light") + initial = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + target = None + for opt in light.locator("option").all(): + v = opt.get_attribute("value") + if v and v != initial: + target = v + break + assert target is not None, "need at least two light themes to test a switch" + light.select_option(value=target) + # Give the change handler a moment to run any cascaded events so they show up in the + # recorded sequence. + page.wait_for_timeout(100) + page.evaluate("window.__versoStopObserver()") + states = page.evaluate("window.__versoThemeStates") + # The only value `data-verso-theme` should take during the switch is the chosen target. + bad = [s for s in states if s != target] + assert not bad, ( + f"intermediate theme states during light-mode switch from {initial!r} to {target!r}: {bad}" + ) + + +def test_switching_light_themes_in_auto_has_no_dark_flash(page): + """In Follow-system mode under `prefers-color-scheme: light`, switching the *light* + dropdown must not paint a dark theme in between.""" + page.emulate_media(color_scheme="light") + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _set_mode(page, "auto") + _expand_choices(page) + light = page.locator("#theme-picker-light") + dark = page.locator("#theme-picker-dark") + page.evaluate( + """() => { + window.__versoThemeStates = []; + const obs = new MutationObserver(records => { + for (const r of records) { + if (r.attributeName === 'data-verso-theme') { + window.__versoThemeStates.push( + document.documentElement.getAttribute('data-verso-theme') + ); + } + } + }); + obs.observe(document.documentElement, { attributes: true }); + window.__versoStopObserver = () => obs.disconnect(); + }""" + ) + initial = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + target = None + for opt in light.locator("option").all(): + v = opt.get_attribute("value") + if v and v != initial: + target = v + break + assert target is not None, "need at least two light themes to test a switch" + dark_value = dark.locator("option").first.get_attribute("value") + light.focus() + light.select_option(value=target) + page.wait_for_timeout(100) + page.evaluate("window.__versoStopObserver()") + states = page.evaluate("window.__versoThemeStates") + # The forbidden state is the *dark* one. Re-applying `initial` (the value the page already + # had) is invisible; only a flash to a different appearance is a real flicker. + assert dark_value not in states, ( + f"dark theme {dark_value!r} appeared during a light-to-light switch; full sequence: {states}" + ) + bad = [s for s in states if s not in (target, initial)] + assert not bad, ( + f"unexpected intermediate themes during auto-mode light switch: {bad} (full: {states})" + ) + + +def test_theme_dropdowns_mark_their_defaults(page): + """The light dropdown marks `defaultLight` with ' (default)' and the dark dropdown marks + `defaultDark` — each appearance's own default, not the other's.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _expand_choices(page) + default_light = page.evaluate("window.versoThemes.defaultLight") + default_dark = page.evaluate("window.versoThemes.defaultDark") + light_marked = page.evaluate( + """() => Array.from(document.querySelectorAll('#theme-picker-light option')) + .filter(o => o.textContent.endsWith(' (default)')).map(o => o.value)""" + ) + dark_marked = page.evaluate( + """() => Array.from(document.querySelectorAll('#theme-picker-dark option')) + .filter(o => o.textContent.endsWith(' (default)')).map(o => o.value)""" + ) + assert light_marked == [default_light], ( + f"light dropdown (default) should mark only {default_light!r}, got {light_marked!r}" + ) + assert dark_marked == [default_dark], ( + f"dark dropdown (default) should mark only {default_dark!r}, got {dark_marked!r}" + ) + + +def test_theme_dropdowns_are_alphabetized(page): + """The Light and Dark theme dropdowns list their themes in alphabetical order by display + name.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _expand_choices(page) + for sel_id in ["#theme-picker-light", "#theme-picker-dark"]: + texts = page.locator(f"{sel_id} option").all_text_contents() + assert texts == sorted(texts), f"{sel_id} options not alphabetised: {texts}" + + +def test_choices_collapsed_by_default(page): + """With nothing customized, the 'Theme choices' section is collapsed (so the picker is a + one-line Appearance dropdown).""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + choices = page.locator("#theme-picker-choices") + assert choices.count() == 1, "expected a collapsible #theme-picker-choices section" + assert choices.get_attribute("open") is None, "choices should start collapsed" + assert not page.locator("#theme-picker-light").is_visible() + + +def test_choices_expanded_when_custom_theme_stored(page, server): + """Once a non-default light theme is stored, the 'Theme choices' section opens by default + on the next load so the customized choice is visible.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + _expand_choices(page) + light = page.locator("#theme-picker-light") + default_light = page.evaluate("window.versoThemes.defaultLight") + chosen = None + for opt in light.locator("option").all(): + v = opt.get_attribute("value") + if v and v != default_light: + chosen = v + break + if chosen is None: + pytest.skip( + "only one light theme registered; cannot store a non-default choice" + ) + light.select_option(value=chosen) + # Reload: a fresh dialog is built, reading the stored non-default light theme. + page.goto(server + "/") + page.wait_for_load_state("domcontentloaded") + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + choices = page.locator("#theme-picker-choices") + assert choices.get_attribute("open") is not None, ( + "choices should be expanded when a non-default theme is stored" + ) + assert page.locator("#theme-picker-light").is_visible() + + +def test_outside_click_dismisses_popover(page): + """Clicking outside the popover closes the dialog and leaves the page on whatever theme + is currently committed.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + initial = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + page.evaluate("document.body.click()") + page.wait_for_function( + "document.getElementById('theme-picker-button').getAttribute('aria-expanded') === 'false'" + ) + assert ( + page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + == initial + ) + + +def test_gear_toggle_close_dismisses_popover(page): + """Clicking the gear a second time closes the dialog without affecting the active theme.""" + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + initial = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + btn.click() + page.wait_for_function( + "document.getElementById('theme-picker-button').getAttribute('aria-expanded') === 'false'" + ) + assert ( + page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + == initial + ) + + +def test_localStorage_disabled_still_loads(page, server): + """When localStorage throws, the page still renders and the default theme is applied.""" + # Stub localStorage *before* navigation so the no-flash script sees the throwing version. + page.add_init_script(""" + Object.defineProperty(window, 'localStorage', { + configurable: true, + get() { throw new Error('storage disabled'); } + }); + """) + page.goto(server + "/") + page.wait_for_load_state("domcontentloaded") + theme = page.evaluate("document.documentElement.getAttribute('data-verso-theme')") + appearance = page.evaluate( + "document.documentElement.getAttribute('data-verso-appearance')" + ) + assert theme is not None and theme != "", ( + "data-verso-theme should be set even without storage" + ) + assert appearance in ("light", "dark"), f"unexpected appearance {appearance!r}" + + +def test_picker_preview_token_hover_shows_tippy(page): + """Hovering a token in the picker's code-sample preview should pop a Tippy tooltip, the + same way it does for tokens in the main page body. + + The picker preview is built on first popover open via `preview.innerHTML = data.codeSample`. + The page's tippy-init script runs at DOMContentLoaded over `document.querySelectorAll( + tokenSelector)` — before the picker preview exists — so without follow-up wiring those + tokens get no `_tippy` instance and hovering them does nothing. + """ + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + preview = page.locator("#theme-picker-preview") + preview.wait_for(state="attached", timeout=5000) + # Pick a real hover-bearing token from the baked sample (e.g. `def greet (...) := ...` + # produces `.const.token` and `.var.token` entries with `data-verso-hover` IDs that + # reference the global `-verso-docs.json`). + token = preview.locator(".token[data-verso-hover]").first + token.wait_for(state="attached", timeout=5000) + has_tippy = page.evaluate( + "el => !!el._tippy", + token.element_handle(), + ) + assert has_tippy, "picker preview token should have a Tippy instance bound" + token.scroll_into_view_if_needed() + token.hover() + # The page-body tippy-init uses `delay: [100, null]`, so allow a brief settle window. + page.wait_for_selector(".tippy-box", state="visible", timeout=3000) + + +def test_picker_preview_binding_highlight(page): + """Hovering an identifier in the picker preview should add `.binding-hl` to its other + occurrences in the preview — the same binding-highlight effect the manual's body code + gets. + """ + btn = _picker_button(page) + btn.click() + _dialog(page).wait_for(state="attached", timeout=5000) + preview = page.locator("#theme-picker-preview") + preview.wait_for(state="attached", timeout=5000) + # The code sample is `def greet (name : String) (count := 1) := ...intercalate count s!"Hello, {name}"`, + # so there are two `.var.token` elements with the same `data-binding` for `name` and two + # for `count`. Pick the first var token's binding, then count its peers before / after + # the hover. + bindings = preview.locator(".token[data-binding^='var-']") + bindings.first.wait_for(state="attached", timeout=5000) + first_binding = bindings.first.get_attribute("data-binding") + assert first_binding, "expected first var token to have a data-binding" + peers = preview.locator(f".token[data-binding='{first_binding}']") + peer_count = peers.count() + assert peer_count >= 2, ( + f"expected at least two `{first_binding}` tokens in the preview, got {peer_count}" + ) + # Hover the first occurrence and confirm the others gain `.binding-hl`. + bindings.first.scroll_into_view_if_needed() + bindings.first.hover() + page.wait_for_function( + f"""() => {{ + const peers = document.querySelectorAll( + "#theme-picker-preview .token[data-binding='{first_binding}']"); + const hl = Array.from(peers).filter(el => el.classList.contains('binding-hl')); + return hl.length === peers.length && peers.length >= 2; + }}""", + timeout=3000, + ) diff --git a/doc/UsersGuide/Manuals.lean b/doc/UsersGuide/Manuals.lean index 57b2c94c4..225eaf9bf 100644 --- a/doc/UsersGuide/Manuals.lean +++ b/doc/UsersGuide/Manuals.lean @@ -304,3 +304,205 @@ The {name}`diagram` code block accepts an `inline` flag that marks it for inline Building PDFs from LaTeX output relies on the `svg` LaTeX package, which calls Inkscape to convert each emitted SVG to PDF at build time. This requires `inkscape` on the `PATH` as well as running `lualatex` with the `-shell-escape` flag. This flag allows LaTeX to execute arbitrary commands during compilation. + +# Themes +%%% +tag := "manual-themes" +%%% + +The manual genre includes support for themes. +Authors may select any number of themes to include, and readers may select any of these themes while reading. +A theme for a manual includes a {ref "output-code-themes"}[code theme], in addition to selecting fonts and colors for the text and navigation interface. + +## Overview +%%% +tag := "manual-themes-overview" +%%% + +When multiple themes are available, the rendered HTML for a manual includes a “gear” button in the header that opens a popover widget. +At the top, an _Appearance_ selector offers radio buttons for _Light_, _Dark_, and _Follow system_. +Beneath it, a collapsible _Theme choices_ section provides dropdown menus to select specific themes for light and dark modes. +The light theme is used in _Light_ mode and the dark theme in _Dark_ mode, while _Follow system_ switches between them automatically based on the browser's `prefers-color-scheme` setting. + +## The `ManualTheme` Structure +%%% +tag := "manual-themes-structure" +%%% + +Authors specify a manual theme as a definition of type {name Verso.Theme.ManualTheme}`ManualTheme`. +Manual themes must be registered using the `@[manual_theme]` attribute. +Manual themes extend {ref "output-code-themes"}[code themes] with fonts and colors for textual content and navigation features. + +{docstring Theme.ManualTheme} + +## Built-In Themes +%%% +tag := "manual-themes-builtins" +%%% + + +```lean -show +open Verso.Theme in +/-- +info: +Alucard (Verso.Theme.ManualTheme.alucard) +Argent (Verso.Theme.ManualTheme.argent) +Beacon Dark (Verso.Theme.ManualTheme.beaconDark) +Beacon Light (Verso.Theme.ManualTheme.beaconLight) +Chromatic Dark (Verso.Theme.ManualTheme.chromaticDark) +Chromatic Light (Verso.Theme.ManualTheme.chromaticLight) +Dracula (Verso.Theme.ManualTheme.dracula) +Hearth Dark (Verso.Theme.ManualTheme.hearthDark) +Hearth Light (Verso.Theme.ManualTheme.hearthLight) +Ink (Verso.Theme.ManualTheme.ink) +Nord (Verso.Theme.ManualTheme.nord) +Sandstone Dark (Verso.Theme.ManualTheme.sandstoneDark) +Sandstone Light (Verso.Theme.ManualTheme.sandstoneLight) +Slate (Verso.Theme.ManualTheme.slate) +Solarized Dark (Verso.Theme.ManualTheme.solarizedDark) +Solarized Light (Verso.Theme.ManualTheme.solarizedLight) +Steel (Verso.Theme.ManualTheme.steel) +-/ +#guard_msgs in +#eval show IO Unit from do + let table : ManualThemeTable := manual_themes% + let entries := table.themes.toList.map + (fun (p : Lean.Name × ManualTheme) => s!"{p.snd.name} ({p.fst})") + IO.println "" + for line in entries.toArray.qsort (· < ·) do + IO.println line +``` + +### Defaults: Ink and Argent +%%% +tag := "manual-default-themes" +%%% + +The default light and dark themes are called _Ink_ and _Argent_, respectively. +These themes use understated formatting, relying on typographical features such as weight and slant syntax and semantic highlighting. + +### Other Included Themes +%%% +tag := "manual-other-themes" +%%% + +:::paragraph +The remaining shipped themes fall into several families, some with both light and dark variants: + +: Chromatic + + The _Chromatic_ themes are versions of _Ink_ and _Argent_ that use color in addition to typographical features for syntax highlighting. + +: Beacon + + The _Beacon_ themes are variants of _Ink_ and _Argent_ that use the [Okabe-Ito palette](https://jfly.uni-koeln.de/color/) to ensure that different colors are distinct for readers with various forms of colorblindness. + +: Solarized + + These themes use Schoonover's [Solarized](https://ethanschoonover.com/solarized/) palettes. + Note that these low-contrast themes are not particularly accessible, and thus should not be used as the default theme for a document. + +: Dracula and Alucard + + _Dracula_ and _Alucard_ implement the [Dracula](https://draculatheme.com/spec) family of themes. + + +: Nord + + Sven Greb's blue-based [Nord](https://www.nordtheme.com/) palette on its Polar Night substrate. + +: Sandstone + + The _Sandstone_ themes are a warm-sepia family: a cream-with-terracotta light variant and a deep canyon-shadow dark variant, both inspired by the deserts of the Southwest USA. + +: Steel and Slate + + _Steel_ and _Slate_ use cool, high-contrast neutral colors. + +: Hearth + + The _Hearth_ themes have a cream-and-sage light variant and a candlelit deep-olive dark variant, and use serif fonts. + +::: + + +## Configuration +%%% +tag := "manual-themes-configuration" +%%% + +The following fields of {name}`RenderConfig` are relevant to themes: + +: {name RenderConfig.availableThemes}`availableThemes` + + This field lists the available themes. By default, it contains all themes that are registered with `@[manual_theme]`. + Authors can restrict readers to a subset of the registered themes by listing the desired themes here. + The default light and dark themes are implicitly considered part of the available theme set. + +: {name RenderConfig.defaultLightTheme}`defaultLightTheme` + + When readers have configured their themes to follow the system preference, this is the default light theme. + +: {name RenderConfig.defaultDarkTheme}`defaultDarkTheme` + + When readers have configured their themes to follow the system preference, this is the default dark theme. + +: {name RenderConfig.defaultAppearance}`defaultAppearance` + + The mode that new readers start in. With {name Verso.Theme.ThemeMode.followSystem}`followSystem` (the default), the picker starts on _Follow system_. With {name Verso.Theme.ThemeMode.light}`light` or {name Verso.Theme.ThemeMode.dark}`dark`, new readers start on that fixed appearance instead, which is useful when a document should default to one appearance regardless of the reader's operating system setting. Readers can always switch in the picker. + +In {name Verso.Theme.ThemeMode.followSystem}`followSystem` mode, readers without JavaScript are served the default light theme, with the default dark theme swapped in via a `prefers-color-scheme: dark` media query, so they follow their system appearance too; in {name Verso.Theme.ThemeMode.light}`light` or {name Verso.Theme.ThemeMode.dark}`dark` mode they are served that appearance's default unconditionally. + +## Accessibility Checking +%%% +tag := "manual-themes-accessibility" +%%% + +By default, manual themes are checked for common accessibility problems, including insufficient contrast between text and background and the use of colors that not all readers can distinguish. +Verso issues a warning when an inaccessible theme is included, and it is an error when an inaccessible theme is the default. +These checks are incomplete: themes may have accessibility problems that are not related to their choices of colors, and the automated tests do not take custom CSS into account. + + +: {name Config.strictThemeCoverage}`strictThemeCoverage` + + Verifies that the set of available themes offers at least one accessible choice for each appearance a reader might select. + With a single available theme, that theme must be accessible; with multiple available themes, at least one accessible light theme and one accessible dark theme must exist. + If {lean}`true` (the default), failing this check is an error. + If {lean}`false`, failing this check results in a warning. + +: {name Config.strictDefaultThemeAccessibility}`strictDefaultThemeAccessibility` + + When {name}`true` (the default), Verso verifies that the configured {name RenderConfig.defaultLightTheme}`defaultLightTheme` and {name RenderConfig.defaultDarkTheme}`defaultDarkTheme` are accessible. + It is an error if either fails the accessibility check. + +: {name Config.warnPerThemeAccessibility}`warnPerThemeAccessibility` + + Emits a build-log warning for every registered theme that has accessibility issues, naming the theme and the specific colors involved. + Defaults to {lean}`true`; set it to {lean}`false` to silence the per-theme advisories. + +### Downgrading Documented Trade-Offs +%%% +tag := "manual-themes-accessibility-downgrade" +%%% + +Not all themes included with Verso are accessible to all readers. +This is intentional on the part of their designers. +For example, the _Solarized_ themes are intentionally low-contrast, and _Beacon Light_ prioritizes the Okabe-Ito palette's distinguishability for many varieties of color perception over contrast. + +By default, Verso warns about these themes if they're included in {name RenderConfig.availableThemes}`availableThemes`. +To silence this warning, set {name Config.warnPerThemeAccessibility}`warnPerThemeAccessibility` to {name}`false`. +By default, it is an error if a non-accessible theme is set as the default theme. +Set {name Config.strictDefaultThemeAccessibility}`strictDefaultThemeAccessibility` to {name}`false` to disable this error. + + +## PDF Output +%%% +tag := "manual-themes-pdf" +%%% + + +PDF output via TeX uses only a {ref "output-code-themes"}[code theme]. +The {name RenderConfig.pdfCodeTheme}`pdfCodeTheme` configuration field selects the code theme to be used to generate PDFs, defaulting to {name Theme.CodeTheme.ink}`ink`. +This setting ignores the theme used for HTML output. +The preamble in the resulting TeX uses `xcolor`'s `\definecolor` to define a named LaTeX color for each themeable color. +Code is generated using _semantic_ macros such as `\versoVar` and `\versoConst`, so a `\renewcommand` is also generated to configure each category. diff --git a/doc/UsersGuide/Output.lean b/doc/UsersGuide/Output.lean index ba2ad0805..a7cb82a13 100644 --- a/doc/UsersGuide/Output.lean +++ b/doc/UsersGuide/Output.lean @@ -5,11 +5,14 @@ Author: David Thrane Christiansen -/ import Lean.DocString.Syntax import VersoManual +import VersoManual.InlineLean import VersoBlog + open Verso Genre Manual open Verso.Genre.Blog (Page Post) +open Verso.Genre.Manual.InlineLean open InlineLean open Verso.Doc @@ -123,3 +126,185 @@ def mkList (xs : List TeX) : TeX := \end{itemize} ``` + +# Themes for Code +%%% +tag := "output-code-themes" +%%% + +A {deftech}_code theme_ is a genre-neutral description of how rendered code should look, including colors, token styling, and font choices. +Any Verso genre can use code themes. +The built-in {name}`Manual` genre extends code themes with further fonts and colors. +Please refer to its {ref "manual-themes"}[theming] documentation for more information. + +A code theme is a value of type {name Theme.CodeTheme}`CodeTheme` with the `@[code_theme]` attribute. + +## Colors and Palettes +%%% +tag := "code-themes-colors" +%%% + +```lean -show +open Verso.Theme +``` + + + +### The `Color` Type and `color%` Literal +%%% +tag := "code-themes-color-type" +%%% + +Colors are represented by the {name}`Color` type. + +{docstring Verso.Theme.Color} + +{docstring Verso.Theme.Color.rgb} + +A number of built-in color constants are provided: + +{docstring Verso.Theme.Color.white} + +{docstring Verso.Theme.Color.black} + +{docstring Verso.Theme.Color.gray} + +{docstring Verso.Theme.Color.red} + +{docstring Verso.Theme.Color.green} + +{docstring Verso.Theme.Color.blue} + +{docstring Verso.Theme.Color.transparent} + +### Named Reference Palettes +%%% +tag := "code-theme-palettes" +%%% + +To support bundled themes, Verso ships with a number of popular color palettes. +Each palette has an associated namespace that contains the named colors from the palette along with a `name : String` and a `sourceLink` of type {name}`SourceLink`, which is a source that can be linked to in theme-selection UIs. + +{docstring Theme.SourceLink} + +: Okabe-Ito + + Masataka Okabe and Kei Ito's eight-hue colorblind-safe palette, published in 2002 as part of their guidance on [accessible color use in scientific visualization](https://jfly.uni-koeln.de/color/). + The hues stay distinguishable under protanopia, deuteranopia, and tritanopia, which makes them a standard reference set for code highlighting that must remain readable to dichromat readers. + The namespace `Verso.Theme.Color.Palettes.OkabeIto` provides {name Verso.Theme.Color.Palettes.OkabeIto.black}`black`, {name Verso.Theme.Color.Palettes.OkabeIto.orange}`orange`, {name Verso.Theme.Color.Palettes.OkabeIto.skyBlue}`skyBlue`, {name Verso.Theme.Color.Palettes.OkabeIto.bluishGreen}`bluishGreen`, {name Verso.Theme.Color.Palettes.OkabeIto.yellow}`yellow`, {name Verso.Theme.Color.Palettes.OkabeIto.blue}`blue`, {name Verso.Theme.Color.Palettes.OkabeIto.vermillion}`vermillion`, and {name Verso.Theme.Color.Palettes.OkabeIto.reddishPurple}`reddishPurple`. + +: Solarized + + Ethan Schoonover's standard cream-on-paper palette of sixteen colors: eight [monotones](https://ethanschoonover.com/solarized/) plus eight accent hues. + Schoonover's rebasing rule splits the monotones by substrate: `base0` and `base1` are dark-mode foreground tones (body text and emphasized content, respectively), `base00` and `base01` are the light-mode counterparts, and the four remaining shades (`base02`, `base03`, `base2`, `base3`) are background and highlight tones for each substrate. + The namespace `Verso.Theme.Color.Palettes.Solarized` provides {name Verso.Theme.Color.Palettes.Solarized.base03}`base03` through {name Verso.Theme.Color.Palettes.Solarized.base3}`base3` for the monotones and {name Verso.Theme.Color.Palettes.Solarized.yellow}`yellow`, {name Verso.Theme.Color.Palettes.Solarized.orange}`orange`, {name Verso.Theme.Color.Palettes.Solarized.red}`red`, {name Verso.Theme.Color.Palettes.Solarized.magenta}`magenta`, {name Verso.Theme.Color.Palettes.Solarized.violet}`violet`, {name Verso.Theme.Color.Palettes.Solarized.blue}`blue`, {name Verso.Theme.Color.Palettes.Solarized.cyan}`cyan`, and {name Verso.Theme.Color.Palettes.Solarized.green}`green` for the accent hues. + +: Dracula and Alucard + + The canonical dark Dracula palette and its light-substrate counterpart Alucard, from the [official Dracula spec](https://draculatheme.com/spec). + Each palette shares twelve color slots — background, current line, selection, foreground, comment, red, orange, yellow, green, cyan, purple, pink — with documented semantic intent that ports the palette into syntax highlighting (pink for keywords, cyan for classes and types, orange for numbers and booleans, yellow for strings, green for functions, purple for instance reserved words, red for errors). + The namespaces `Verso.Theme.Color.Palettes.DraculaClassic` and `Verso.Theme.Color.Palettes.AlucardClassic` each provide the twelve named colors. + +: Nord + + Sven Greb's arctic, north-bluish palette of sixteen colors organized in [four groups](https://www.nordtheme.com/docs/colors-and-palettes): *Polar Night* ({name Verso.Theme.Color.Palettes.Nord.nord0}`nord0` through {name Verso.Theme.Color.Palettes.Nord.nord3}`nord3`) for dark-substrate backgrounds and code surfaces, *Snow Storm* ({name Verso.Theme.Color.Palettes.Nord.nord4}`nord4` through {name Verso.Theme.Color.Palettes.Nord.nord6}`nord6`) for body text on dark backgrounds and substrates on light variants, *Frost* ({name Verso.Theme.Color.Palettes.Nord.nord7}`nord7` through {name Verso.Theme.Color.Palettes.Nord.nord10}`nord10`) for the canonical syntax accents, and *Aurora* ({name Verso.Theme.Color.Palettes.Nord.nord11}`nord11` through {name Verso.Theme.Color.Palettes.Nord.nord15}`nord15`) for warm accent hues used by diagnostics and additional syntax categories. + The namespace `Verso.Theme.Color.Palettes.Nord` provides each numbered constant. + +## Fonts and Typefaces +%%% +tag := "code-themes-fonts" +%%% + +The {name}`Typeface` type represents a general typeface. +There are three built-in faces, {name}`Typeface.sans`, {name}`Typeface.serif`, and {name}`Typeface.mono`, which stand for unspecified sans-serif, serif, and monospaced font faces. +Specific font faces may be provided using the {name}`Typeface.files` constructor, which bundles font files with sufficient metadata to use them in a theme. + +{docstring Typeface} + + +### `define_font_face` +%%% +tag := "code-themes-fonts-def" +%%% + +To make it easier to include custom fonts, Verso provides the `define_font_face` command, which declares a {name}`FontFace` value by name and embeds the font file into the resulting `.olean` at compile time. +This allows themes that include fonts to be distributed as ordinary Lean libraries. + +{docstring Verso.defineFontFace} + +These {name}`FontFace` declarations are then composed into a {name}`Typeface` via the {name}`Typeface.files` constructor. + +## The `CodeTheme` Structure +%%% +tag := "code-themes-structure" +%%% + +{docstring Theme.CodeTheme} + +Remember to register code themes using the `@[code_theme]` attribute. + +## Accessibility Checking +%%% +tag := "code-themes-accessibility" +%%% + +Code themes are checked for accessibility. +These checks are by nature incomplete: they can discover the _presence_ of problems, but not their absence. +Nonetheless, ensuring that the default theme used by a document passes these tests is a good first step towards accessibility. + +{docstring Theme.CodeTheme.checkAccessibility} + +The check compares the color fields of a {name Theme.CodeTheme}`CodeTheme` and returns an array of {name Theme.Color.Issue}`Issue` values, one per problem found. + +Themes may contain arbitrary CSS. +In this case, some other means of checking accessibility should be used. + +### Contrast +%%% +tag := "code-themes-accessibility-contrast" +%%% +The contrast checker uses two thresholds: WCAG AA's 4.5:1 ratio for primary text and 3:1 for UI accents and large-text positions. + +The following contrasts are checked at the text threshold (4.5:1): + + * Body, error-message, warning-message, and info-message text against the page background. + * Each themed token color against the code-block background. + * The code color against the inline-code background, when one is set. + * The code color against both highlight backgrounds, and body text against the prose-highlight background. + * Hover-popup text against the hover-popup background and against the tactic-state background. + * Code against the tactic-state background. + +The following contrasts are checked at the large text threshold (3:1): + + * Each diagnostic accent (error, warning, info indicator) against the page background. + * The neutral UI-element color against the code-block background. + * The tactic-state border against the tactic-state background. + +Images that contain text are not automatically checked, and must be checked for accessibility in some other way. + +### Color Perception +%%% +tag := "code-themes-accessibility-perception" +%%% + +The eleven token colors are checked for perceptual distinctness in four separate modes: + * unmodified + * simulated protanopia + * simulated deuteranopia + * simulated tritanopia. + +Every pair must remain perceptibly distinct (CIEDE2000 ΔE above a tunable threshold). +A pair of _identical_ colors is not an issue, because such themes have explicitly decided not to distinguish that pair using color. + +A translucent foreground is composited over its background (via {name Theme.Color.over}`Color.over`) before checking. +A translucent _background_, by contrast, is itself reported as a contrast issue, because the effective backdrop is unknown. + + +### The `Issue` Type +%%% +tag := "code-themes-accessibility-issues" +%%% + +Issues are reported using the type {name Theme.Color.Issue}`Issue`, which describes the accessibility issue. + +{docstring Theme.Color.Issue} diff --git a/generate.sh b/generate.sh index efd020c8d..b5bd058f1 100755 --- a/generate.sh +++ b/generate.sh @@ -2,7 +2,21 @@ set -e -if ! command -v inkscape >/dev/null 2>&1; then +html_only=false +for arg in "$@"; do + case "$arg" in + --html) + html_only=true + ;; + *) + echo "Unknown argument: $arg" >&2 + echo "Usage: $0 [--html]" >&2 + exit 2 + ;; + esac +done + +if [ "$html_only" = false ] && ! command -v inkscape >/dev/null 2>&1; then if [ -f "/Applications/Inkscape.app/Contents/MacOS/inkscape" ]; then PATH="$PATH:/Applications/Inkscape.app/Contents/MacOS" else @@ -11,20 +25,25 @@ if ! command -v inkscape >/dev/null 2>&1; then fi fi -echo "Building the user's guide as TeX and HTML" -lake exe usersguide --delay-html-multi multi.json --delay-html-single single.json --with-tex -lake exe usersguide --resume-html-multi multi.json --resume-html-single single.json +if [ "$html_only" = true ]; then + echo "Building the user's guide as HTML" + lake exe usersguide +else + echo "Building the user's guide as TeX and HTML" + lake exe usersguide --delay-html-multi multi.json --delay-html-single single.json --with-tex + lake exe usersguide --resume-html-multi multi.json --resume-html-single single.json -echo "Building the user's guide as PDF" -mkdir -p _out/tex -pushd _out/tex -lualatex -shell-escape main -lualatex -shell-escape main -lualatex -shell-escape main -popd + echo "Building the user's guide as PDF" + mkdir -p _out/tex + pushd _out/tex + lualatex -shell-escape main + lualatex -shell-escape main + lualatex -shell-escape main + popd -echo "User's guide PDF is at:" -readlink -f _out/tex/main.pdf + echo "User's guide PDF is at:" + readlink -f _out/tex/main.pdf +fi echo "HTML is at:" readlink -f _out/html-single/index.html diff --git a/lakefile.lean b/lakefile.lean index cea6eac61..89750d2af 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -134,6 +134,15 @@ lean_exe «verso-tests» where srcDir := "src/tests" supportInterpreter := true +lean_lib ThemeTestDoc where + srcDir := "src/tests" + roots := #[`ThemeTestDoc] + +lean_exe «theme-test-site» where + root := `ThemeTestMain + srcDir := "src/tests" + supportInterpreter := true + lean_lib UsersGuide where srcDir := "doc" leanOptions := #[⟨`weak.linter.verso.manual.headerTags, true⟩] diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index f77fde9bc..2827698ba 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -57,7 +57,8 @@ def testTexOutput let runTest : IO Unit := open Verso Genre Manual in do let logger ← Verso.Logger.new - emitTeX versoConfig doc.toPart |>.run extension_impls% |>.run logger + emitTeX ({ versoConfig with : RenderConfig }) doc.toPart + |>.run ({} : Verso.Theme.ThemeRegistry) |>.run extension_impls% |>.run logger Verso.Integration.runTests { config with testDir := "src/tests/integration" / dir, @@ -149,12 +150,49 @@ def testSerialization (_ : Config) : IO Unit := do if fails > 0 then throw <| IO.userError s!"{fails} serialization tests failed" +def testColorMath (_ : Config) : IO Unit := do + IO.println "Running color math tests..." + let fails ← runColorMathTests + if fails > 0 then + throw <| IO.userError s!"{fails} color math tests failed" + +def testColorAccessibility (_ : Config) : IO Unit := do + IO.println "Running color accessibility tests..." + let fails ← runColorAccessibilityTests + if fails > 0 then + throw <| IO.userError s!"{fails} color accessibility tests failed" + def testSearchJs (_ : Config) : IO Unit := do IO.println "Running search JS wire-format tests..." let fails ← Verso.Tests.SearchJs.runSearchJsTests if fails > 0 then throw <| IO.userError s!"{fails} search JS tests failed" +open Verso in +/-- +Golden test for the default code theme's generated CSS. The expected fixture lives at +`src/tests/golden/theme-css/default.expected` and is regenerated with `--update-expected`. +-/ +def testThemeCss (cfg : Config) : IO Unit := do + IO.println "Running theme CSS golden test..." + let runTest (input : String) : IO String := do + let name := input.trimAscii + if name == "default" then + let varsBlock := s!":root \{\n{Theme.CodeTheme.ink.cssVariables}}\n" + let combined := varsBlock ++ "\n" ++ Code.highlightingStyle + -- Trim the trailing blank lines `highlightingStyle` ships with so the golden file + -- ends with a single newline (otherwise `git diff --check` flags the EOF blank). + let mut out := combined + while out.endsWith "\n\n" do out := (out.dropEnd 1).copy + return out + else + throw <| IO.userError s!"Unknown theme: {name}" + GoldenTest.runTests { + testDir := "src/tests/golden/theme-css", + updateExpected := cfg.updateExpected, + runTest + } + def testBlog (_ : Config) : IO Unit := do IO.println "Running blog tests with Plausible..." let fails ← runBlogTests @@ -349,9 +387,43 @@ def testBuildLog (_ : Config) : IO Unit := do throw <| IO.userError "redirected logging should still accumulate into the logger's buffers" IO.println " All build-log tests passed." +open Verso Theme in +def testColor (_ : Config) : IO Unit := do + IO.println "Running color tests..." + let check (name got expected : String) : IO Unit := + unless got == expected do + throw <| IO.userError s!"{name}: got \"{got}\", expected \"{expected}\"" + -- Opaque colors render as lowercase `#rrggbb`. + check "black.css" Color.black.css "#000000" + check "white.css" Color.white.css "#ffffff" + check "gray.css" Color.gray.css "#808080" + check "red.css" Color.red.css "#ff0000" + check "green.css" Color.green.css "#008000" + check "blue.css" Color.blue.css "#0000ff" + check "transparent.css" Color.transparent.css "#00000000" + check "6-digit literal css" (color%#4777ff).css "#4777ff" + -- A 3-digit literal doubles each digit. + check "3-digit literal css" (color%#fff).css "#ffffff" + -- A color with alpha renders as `rgba(...)` with the alpha in [0, 1]. + check "alpha literal css" (color%#aabbcc80).css "#aabbcc80" + -- TeX rendering is six uppercase hex digits with no alpha. + check "red.tex" Color.red.tex "FF0000" + check "literal tex" (color%#4777ff).tex "4777FF" + check "alpha literal tex" (color%#aabbcc80).tex "AABBCC" + -- The literal parses to the expected channels. + unless (color%#4777ff) = Color.rgba 0x47 0x77 0xff 255 do + throw <| IO.userError "6-digit literal parsed to the wrong channels" + unless (color%#fff) = Color.rgba 255 255 255 255 do + throw <| IO.userError "3-digit literal parsed to the wrong channels" + IO.println " All color tests passed." + open Verso.Integration in def tests := [ testBuildLog, + testColor, + testColorMath, + testColorAccessibility, + testThemeCss, testSerialization, testSearchJs, testBlog, diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean index 9b25d3df0..136521bd2 100644 --- a/src/tests/Tests.lean +++ b/src/tests/Tests.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ import Tests.Basic +import Tests.Color +import Tests.ColorAccessibility +import Tests.ColorMath import Tests.Elab +import Tests.Font import Tests.GenericCode import Tests.Golden import Tests.CommentSkipping diff --git a/src/tests/Tests/Arbitrary.lean b/src/tests/Tests/Arbitrary.lean index bfe69e9a8..decd6b82c 100644 --- a/src/tests/Tests/Arbitrary.lean +++ b/src/tests/Tests/Arbitrary.lean @@ -18,6 +18,7 @@ public meta import VersoManual.LicenseInfo public meta import VersoSearch public meta import VersoSearch.DomainSearch public meta import Verso.Output.Html +public meta import Verso.Theme.Color.Types public meta import MultiVerso.Manifest public meta import VersoManual.Basic import all VersoManual.Basic @@ -437,3 +438,18 @@ instance : Shrinkable System.FilePath where if let some parent := path.parent then parent :: (path.fileName.toList.flatMap shrink |>.map path.withFileName) else [] + +instance : Arbitrary Verso.Theme.Color where + arbitrary := do + -- Bias the alpha channel: fully opaque (the common case) 60% of the time, fully transparent 5%, + -- and uniformly random the rest. A uniform alpha would almost never be exactly opaque. + let a ← frequency (pure 255) [(60, pure 255), (5, pure 0), (35, arbitrary)] + return .rgba (← arbitrary) (← arbitrary) (← arbitrary) a + +instance : Shrinkable Verso.Theme.Color where + shrink + | .rgba r g b a => + (shrink r |>.map (Verso.Theme.Color.rgba · g b a)) ++ + (shrink g |>.map (Verso.Theme.Color.rgba r · b a)) ++ + (shrink b |>.map (Verso.Theme.Color.rgba r g · a)) ++ + (shrink a |>.map (Verso.Theme.Color.rgba r g b ·)) diff --git a/src/tests/Tests/Color.lean b/src/tests/Tests/Color.lean new file mode 100644 index 000000000..834db3ef4 --- /dev/null +++ b/src/tests/Tests/Color.lean @@ -0,0 +1,56 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Verso.Theme.Color +import Lean.Elab.Command + +/-! +Compile-time tests for the `color%` literal: the three accepted hex lengths elaborate, and other +lengths are rejected with a clear error. Value-level `css`/`tex` checks live in the runtime suite +(`testColor` in `TestMain`). +-/ + +open Verso + +-- The three accepted lengths elaborate and render as expected (a 3-digit literal doubles each +-- digit; 8 digits keep the alpha byte). +/-- info: #ffffff -/ +#guard_msgs in +#eval IO.println (color%#fff).css + +/-- info: #4777ff -/ +#guard_msgs in +#eval IO.println (color%#4777ff).css + +/-- info: #aabbcc80 -/ +#guard_msgs in +#eval IO.println (color%#aabbcc80).css + +/-- error: expected 3, 6, or 8 hex digits, got 0 -/ +#guard_msgs in +example : Color := color%# + +/-- error: expected 3, 6, or 8 hex digits, got 4 -/ +#guard_msgs in +example : Color := color%#1234 + +/-- error: expected 3, 6, or 8 hex digits, got 5 -/ +#guard_msgs in +example : Color := color%#12345 + +/-- error: expected 3, 6, or 8 hex digits, got 7 -/ +#guard_msgs in +example : Color := color%#1234567 + +-- The parser registers trailing whitespace on the hex token, so the original source (including the +-- spaces after the literal) can be reconstructed from the parse tree by `Syntax.reprint`. +open Lean Parser in +/-- info: round-trips: true -/ +#guard_msgs in +#eval show Lean.Elab.Command.CommandElabM Unit from do + let input := "color%#abc " + match runParserCategory (← getEnv) `term input with + | .ok stx => IO.println s!"round-trips: {stx.reprint == some input}" + | .error e => throwError e diff --git a/src/tests/Tests/ColorAccessibility.lean b/src/tests/Tests/ColorAccessibility.lean new file mode 100644 index 000000000..c0a7fcd95 --- /dev/null +++ b/src/tests/Tests/ColorAccessibility.lean @@ -0,0 +1,162 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import Plausible +public meta import Verso.Theme.Color +public meta import VersoManual.Theme +public meta import VersoManual.Theme.Defaults +public meta import Tests.Arbitrary + +/-! +Unit and property tests for the accessibility predicates and checks in `Verso.Theme.Color.Accessibility`. +-/ + +open Plausible Gen Arbitrary Shrinkable +open Verso Verso.Theme Verso.Theme.Color + +meta section + +/-- The Okabe-Ito colorblind-safe palette, used to validate the distinguishability threshold. -/ +def okabeIto : Array (String × Color) := #[ + ("black", color%#000000), + ("orange", color%#e69f00), + ("sky blue", color%#56b4e9), + ("bluish green", color%#009e73), + ("yellow", color%#f0e442), + ("blue", color%#0072b2), + ("vermillion", color%#d55e00), + ("reddish purple", color%#cc79a7), +] + +/-! ## Unit tests on curated palettes -/ + +-- A high-contrast pair (black on white) passes the text contrast check. +/-- info: true -/ +#guard_msgs in +#eval (contrastIssues textContrastThreshold "black on white" .black .white).isEmpty + +-- A low-contrast pair (gray on white, ratio ≈ 3.95) fails the text contrast check. +/-- info: false -/ +#guard_msgs in +#eval (contrastIssues textContrastThreshold "gray on white" .gray .white).isEmpty + +-- A nearly-opaque (99%) black composited over white is essentially black, so it passes easily. +/-- info: true -/ +#guard_msgs in +#eval (contrastIssues textContrastThreshold "99% black on white" (color%#000000fc) .white).isEmpty + +-- A half-transparent black over white composites to mid-gray, which fails the text threshold. +/-- info: false -/ +#guard_msgs in +#eval (contrastIssues textContrastThreshold "50% black on white" (color%#00000080) .white).isEmpty + +-- A translucent background cannot be contrast-checked: the effective backdrop is unknown. +/-- info: false -/ +#guard_msgs in +#eval (contrastIssues textContrastThreshold "black on translucent" .black (color%#ffffff80)).isEmpty + +-- A red and a green of matched lightness collapse together under deuteranopia (ΔE ≈ 2.1). +/-- info: false -/ +#guard_msgs in +#eval (colorblindIssues distinguishableThreshold #[("red", color%#e60000), ("green", color%#00a000)]).isEmpty + +-- Okabe-Ito blue and orange stay distinct under every dichromacy. +/-- info: true -/ +#guard_msgs in +#eval (colorblindIssues distinguishableThreshold #[("blue", color%#0072b2), ("orange", color%#e69f00)]).isEmpty + +-- The whole colorblind-safe Okabe-Ito palette passes the distinguishability check. +/-- info: true -/ +#guard_msgs in +#eval (colorblindIssues distinguishableThreshold okabeIto).isEmpty + +-- A pair of identical colors is not a colorblind issue: the theme is not relying on color to +-- distinguish them (it might be using weight or style instead, as the default theme does). +/-- info: true -/ +#guard_msgs in +#eval (colorblindIssues distinguishableThreshold #[("a", .black), ("b", .black)]).isEmpty + +/-! ## `ManualTheme.checkAccessibility` -/ + +-- The shipped default theme passes its own accessibility check. +/-- info: true -/ +#guard_msgs in +#eval ManualTheme.ink.checkAccessibility.isEmpty + +-- A low-contrast override (gray text on a near-white background) is flagged as a contrast +-- problem (one per evaluated text pair against the page background). +private def lowContrastTheme : ManualTheme := { + ManualTheme.ink with + textColor := color%#bbbbbb, +} + +/-- info: true -/ +#guard_msgs in +#eval (lowContrastTheme.checkAccessibility.any (·.kind == .contrast)) + +-- A token palette that collapses under deuteranopia (a red and a green of matched lightness) +-- is flagged as a CVD problem. +private def cvdTheme : ManualTheme := { + ManualTheme.ink with + const.color := color%#e60000, + keyword.color := color%#00a000, +} + +/-- info: true -/ +#guard_msgs in +#eval (cvdTheme.checkAccessibility.any (·.kind == .colorblind)) + +-- The contrast and colorblind checks are independent: the low-contrast theme has no colorblind +-- issues, and the CVD theme has no contrast issues against the page background. +/-- info: false -/ +#guard_msgs in +#eval (lowContrastTheme.checkAccessibility.any (·.kind == .colorblind)) + +-- A theme whose `highlightColor` is too close to `textColor` is flagged: search results render +-- matched terms with `highlightColor` as their background, so the body text must read on it. +private def badHighlightTheme : ManualTheme := { + ManualTheme.ink with + highlightColor := color%#333333, +} + +/-- info: true -/ +#guard_msgs in +#eval (badHighlightTheme.checkAccessibility.any (fun i => + i.kind == .contrast && (i.message.splitOn "highlight").length > 1)) + +/-! ## Property tests -/ + +open scoped Plausible.Decorations in +def testProp + (p : Prop) (cfg : Configuration := {}) + (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : + IO (TestResult p') := + Testable.checkIO p' (cfg := cfg) + +/-- Contrast is monotone in the threshold: passing at 4.5 implies passing at 3.0. -/ +def testContrastMonotone := testProp <| ∀ (fg bg : Color), + !meetsContrast 4.5 fg bg || meetsContrast 3.0 fg bg + +/-- When the contrast check reports no problem, the composited foreground meets the contrast. -/ +def testNoContrastIssueMeansMeets := testProp <| ∀ (fg bg : Color), + !(contrastIssues 4.5 "pair" fg bg).isEmpty || meetsContrast 4.5 (over fg bg) bg + +open Lean (Name) + +def colorAccessibilityTests : List (Name × (Σ p, IO <| TestResult p)) := [ + (`testContrastMonotone, ⟨_, testContrastMonotone⟩), + (`testNoContrastIssueMeansMeets, ⟨_, testNoContrastIssueMeansMeets⟩), +] + +public def runColorAccessibilityTests : IO Nat := do + let mut failures := 0 + for (name, test) in colorAccessibilityTests do + IO.print s!"{name}: " + let res ← test.2 + IO.println res + unless res matches .success .. do + failures := failures + 1 + return failures diff --git a/src/tests/Tests/ColorMath.lean b/src/tests/Tests/ColorMath.lean new file mode 100644 index 000000000..a68904b4b --- /dev/null +++ b/src/tests/Tests/ColorMath.lean @@ -0,0 +1,350 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import Plausible +public meta import Verso.Theme.Color +import all Verso.Theme.Color.Math +public meta import Tests.Arbitrary + +/-! +Unit and property tests for the color math in `Verso.Theme.Color.Math`. +-/ + +open Plausible Gen Arbitrary Shrinkable +open Verso Verso.Theme Verso.Theme.Color + +meta section + +/-- Approximate float equality to a tolerance. -/ +def approx (ε a b : Float) : Bool := (a - b).abs ≤ ε + +/-- Whether two colors' channels are all within `ε` of each other. -/ +def channelsClose (ε : Nat) : Color → Color → Bool + | .rgba r1 g1 b1 a1, .rgba r2 g2 b2 a2 => + let near (x y : UInt8) : Bool := (Int.ofNat x.toNat - Int.ofNat y.toNat).natAbs ≤ ε + near r1 r2 && near g1 g2 && near b1 b2 && near a1 a2 + +instance : Arbitrary CVD where + arbitrary := Gen.elements [.protanopia, .deuteranopia, .tritanopia] (by simp) + +instance : Shrinkable CVD where + shrink _ := [] + +/-! ## Unit tests on reference values -/ + +-- Relative luminance of black is 0 and of white is 1, so their contrast ratio is the maximal 21. +/-- info: (0.000000, 1.000000, 21.000000) -/ +#guard_msgs in +#eval (relativeLuminance .black, relativeLuminance .white, contrastRatio .black .white) + +-- ΔE is zero for equal colors and large for black vs. white. +/-- info: (0.000000, 100.000004) -/ +#guard_msgs in +#eval (deltaE .black .black, deltaE .white .black) + +-- Dichromacy simulation leaves the gray axis unchanged. +/-- info: (Verso.Theme.Color.rgba 128 128 128 255, Verso.Theme.Color.rgba 128 128 128 255, Verso.Theme.Color.rgba 128 128 128 255) -/ +#guard_msgs in +#eval (dichromacy .protanopia .gray, dichromacy .deuteranopia .gray, dichromacy .tritanopia .gray) + +-- Red and green, far apart normally, collapse closer together under deuteranopia. +/-- info: true -/ +#guard_msgs in +#eval deltaE (dichromacy .deuteranopia .red) (dichromacy .deuteranopia .green) < deltaE .red .green + +/-! ## Property tests -/ + +open scoped Plausible.Decorations in +def testProp + (p : Prop) (cfg : Configuration := {}) + (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : + IO (TestResult p') := + Testable.checkIO p' (cfg := cfg) + +/-- Relative luminance lies in [0, 1]. -/ +def testLuminanceRange := testProp <| ∀ (c : Color), + 0.0 ≤ relativeLuminance c ∧ relativeLuminance c ≤ 1.000000001 + +/-- Raises a channel by `d`, saturating at 255. -/ +private def raise (x d : UInt8) : UInt8 := UInt8.ofNat (Nat.min 255 (x.toNat + d.toNat)) + +/-- Raising any channel never lowers the relative luminance. -/ +def testLuminanceMonotone := testProp <| ∀ (r g b d0 d1 d2 : UInt8), + relativeLuminance (.rgba r g b 255) + ≤ relativeLuminance (.rgba (raise r d0) (raise g d1) (raise b d2) 255) + 0.000000001 + +/-- Contrast ratio is symmetric. -/ +def testContrastSymmetric := testProp <| ∀ (c d : Color), + approx 0.000000001 (contrastRatio c d) (contrastRatio d c) + +/-- Contrast ratio lies in [1, 21]. -/ +def testContrastRange := testProp <| ∀ (c d : Color), + 0.999999999 ≤ contrastRatio c d ∧ contrastRatio c d ≤ 21.000000001 + +/-- A color has contrast ratio 1 with itself. -/ +def testContrastSelf := testProp <| ∀ (c : Color), + approx 0.000000001 (contrastRatio c c) 1.0 + +/-- ΔE is non-negative. -/ +def testDeltaENonneg := testProp <| ∀ (c d : Color), deltaE c d ≥ 0.0 + +/-- ΔE is symmetric. -/ +def testDeltaESymmetric := testProp <| ∀ (c d : Color), + approx 0.0001 (deltaE c d) (deltaE d c) + +/-- ΔE is zero for equal colors. -/ +def testDeltaEZero := testProp <| ∀ (c : Color), approx 0.000001 (deltaE c c) 0.0 + +/-- Dichromacy maps the gray axis to itself (within one quantization step). -/ +def testDichromacyGray := testProp <| ∀ (cvd : CVD) (v : UInt8), + channelsClose 1 (dichromacy cvd (.rgba v v v 255)) (.rgba v v v 255) + +/-- The alpha channel of a color. -/ +private def alphaOf : Color → UInt8 + | .rgba _ _ _ a => a + +/-- +Dichromacy preserves the alpha channel. + +It is *not* idempotent on the quantized, gamut-clamped `Color`: clipping a channel to 0 or 255 +discards the exact projected point, so a second pass can drift. Idempotence holds only for the +continuous linear-light projection. +-/ +def testDichromacyAlphaPreserved := testProp <| ∀ (cvd : CVD) (c : Color), + alphaOf (dichromacy cvd c) == alphaOf c + +/-- Relative luminance ignores the alpha channel. -/ +def testLuminanceIgnoresAlpha := testProp <| ∀ (r g b a : UInt8), + relativeLuminance (.rgba r g b a) == relativeLuminance (.rgba r g b 255) + +/-- Replaces a color's alpha channel with full opacity. -/ +private def «opaque» : Color → Color + | .rgba r g b _ => .rgba r g b 255 + +/-- Contrast ratio ignores the alpha channel. -/ +def testContrastIgnoresAlpha := testProp <| ∀ (c1 c2 : Color), + contrastRatio c1 c2 == contrastRatio («opaque» c1) («opaque» c2) + +/-- ΔE ignores the alpha channel. -/ +def testDeltaEIgnoresAlpha := testProp <| ∀ (c1 c2 : Color), + deltaE c1 c2 == deltaE («opaque» c1) («opaque» c2) + +/-- +Deuteranopia collapses pure red and pure green toward each other: the simulated ΔE between +{lit}`(r, 0, 0)` and {lit}`(0, g, 0)` never exceeds the original ΔE (within a small numerical +tolerance for sRGB round-trip and 8-bit rounding). + +`≤` rather than strict `<` because the degenerate `r = g = 0` case has both colors equal to +black and both ΔEs equal to zero. The strict inequality is exercised by the targeted +spot-check {Lean.Doc.name}`testDeuteranopiaRedGreenSpotCheck` below, which uses pure-saturated +red and green so the collapse is unambiguous. +-/ +def testDeuteranopiaCollapsesRedGreen := testProp <| ∀ (r g : UInt8), + let red : Color := .rgba r 0 0 255 + let green : Color := .rgba 0 g 0 255 + let simRed := dichromacy .deuteranopia red + let simGreen := dichromacy .deuteranopia green + -- A tiny tolerance absorbs sRGB encode-decode round-trip plus 8-bit rounding noise on the + -- ΔE pipeline. Without it the inequality can flip by ~1e-3 at boundary inputs. + deltaE simRed simGreen ≤ deltaE red green + 0.001 + +/-- +Spot check: pure saturated red and pure saturated green are far apart normally but collapse +much closer together under deuteranopia. Asserts the simulated ΔE drops to less than half the +unsimulated one — well outside any quantization noise band, so the directionality of the +collapse is what the test actually exercises (where the bounded-form property +{Lean.Doc.name}`testDeuteranopiaCollapsesRedGreen` only asserts non-increase). +-/ +def testDeuteranopiaRedGreenSpotCheck := testProp <| + let red : Color := .rgba 255 0 0 255 + let green : Color := .rgba 0 255 0 255 + let simRed := dichromacy .deuteranopia red + let simGreen := dichromacy .deuteranopia green + deltaE simRed simGreen < deltaE red green / 2 + +open Lean (Name) + +def colorMathTests : List (Name × (Σ p, IO <| TestResult p)) := [ + (`testLuminanceRange, ⟨_, testLuminanceRange⟩), + (`testLuminanceMonotone, ⟨_, testLuminanceMonotone⟩), + (`testContrastSymmetric, ⟨_, testContrastSymmetric⟩), + (`testContrastRange, ⟨_, testContrastRange⟩), + (`testContrastSelf, ⟨_, testContrastSelf⟩), + (`testDeltaENonneg, ⟨_, testDeltaENonneg⟩), + (`testDeltaESymmetric, ⟨_, testDeltaESymmetric⟩), + (`testDeltaEZero, ⟨_, testDeltaEZero⟩), + (`testDichromacyGray, ⟨_, testDichromacyGray⟩), + (`testDichromacyAlphaPreserved, ⟨_, testDichromacyAlphaPreserved⟩), + (`testLuminanceIgnoresAlpha, ⟨_, testLuminanceIgnoresAlpha⟩), + (`testContrastIgnoresAlpha, ⟨_, testContrastIgnoresAlpha⟩), + (`testDeltaEIgnoresAlpha, ⟨_, testDeltaEIgnoresAlpha⟩), + (`testDeuteranopiaCollapsesRedGreen, ⟨_, testDeuteranopiaCollapsesRedGreen⟩), + (`testDeuteranopiaRedGreenSpotCheck, ⟨_, testDeuteranopiaRedGreenSpotCheck⟩), +] + +public def runColorMathTests : IO Nat := do + let mut failures := 0 + for (name, test) in colorMathTests do + IO.print s!"{name}: " + let res ← test.2 + IO.println res + unless res matches .success .. do + failures := failures + 1 + return failures + +/-! +## Source-backed simulation cases + +`cvdReferenceVectors` are outputs of DaltonLens-Python's `Simulator_Brettel1997` (severity 1.0), the +reference implementation that libDaltonLens is validated against. Each row is +`(input, protanopia, deuteranopia, tritanopia)`. `dichromacy` is expected to match each within a +couple of byte units: the small difference comes from libDaltonLens's matrix coefficients being +rounded to five decimals, not from a different method. A large deviation would mean a transposed +matrix, wrong half-plane sign, wrong gamma direction, or swapped channels. +-/ + +def cvdReferenceVectors : List (Color × Color × Color × Color) := [ + (.rgba 0 0 0 255, .rgba 0 0 0 255, .rgba 0 0 0 255, .rgba 0 0 0 255), + (.rgba 255 255 255 255, .rgba 254 254 254 255, .rgba 254 254 254 255, .rgba 254 254 254 255), + (.rgba 128 128 128 255, .rgba 128 128 128 255, .rgba 128 128 128 255, .rgba 128 128 128 255), + (.rgba 255 0 0 255, .rgba 106 90 13 255, .rgba 163 138 0 255, .rgba 254 0 78 255), + (.rgba 0 128 0 255, .rgba 139 118 0 255, .rgba 120 103 17 255, .rgba 58 117 135 255), + (.rgba 0 0 255 255, .rgba 0 54 254 255, .rgba 0 86 254 255, .rgba 0 95 134 255), + (.rgba 255 255 0 255, .rgba 254 250 0 255, .rgba 254 242 21 255, .rgba 254 239 242 255), + (.rgba 0 255 255 255, .rgba 238 242 254 255, .rgba 209 223 254 255, .rgba 73 248 254 255), + (.rgba 255 0 255 255, .rgba 0 105 254 255, .rgba 101 160 251 255, .rgba 238 98 120 255), + (.rgba 29 3 65 255, .rgba 0 13 65 255, .rgba 0 23 64 255, .rgba 14 21 23 255), + (.rgba 220 20 60 255, .rgba 87 81 62 255, .rgba 139 121 49 255, .rgba 220 12 72 255), + (.rgba 0 128 255 255, .rgba 0 129 254 255, .rgba 0 132 254 255, .rgba 0 147 185 255), + (.rgba 217 163 130 255, .rgba 181 168 130 255, .rgba 191 176 128 255, .rgba 220 158 164 255), + (.rgba 69 78 10 255, .rgba 88 75 9 255, .rgba 84 71 12 255, .rgba 75 72 73 255), + (.rgba 19 4 44 255, .rgba 0 8 44 255, .rgba 0 15 43 255, .rgba 9 13 15 255), + (.rgba 208 166 233 255, .rgba 144 174 233 255, .rgba 164 185 231 255, .rgba 198 176 178 255), + (.rgba 128 155 248 255, .rgba 98 157 248 255, .rgba 107 160 247 255, .rgba 105 168 190 255), + (.rgba 186 161 139 255, .rgba 171 163 139 255, .rgba 175 165 138 255, .rgba 188 157 160 255), + (.rgba 143 239 71 255, .rgba 254 226 68 255, .rgba 237 207 80 255, .rgba 173 222 242 255), + (.rgba 208 171 0 255, .rgba 200 172 0 255, .rgba 202 173 0 255, .rgba 217 159 165 255), + (.rgba 100 219 141 255, .rgba 228 207 140 255, .rgba 204 189 144 255, .rgba 130 206 233 255), + (.rgba 8 195 186 255, .rgba 185 185 185 255, .rgba 162 169 187 255, .rgba 60 188 223 255), + (.rgba 216 44 22 255, .rgba 99 86 26 255, .rgba 142 121 0 255, .rgba 217 32 77 255), + (.rgba 220 5 138 255, .rgba 43 82 138 255, .rgba 124 126 133 255, .rgba 215 46 82 255), + (.rgba 20 76 123 255, .rgba 43 74 122 255, .rgba 38 73 123 255, .rgba 0 81 99 255), + (.rgba 108 103 7 255, .rgba 118 101 6 255, .rgba 116 99 9 255, .rgba 114 96 97 255), + (.rgba 1 31 2 255, .rgba 34 28 1 255, .rgba 28 23 3 255, .rgba 9 27 33 255), + (.rgba 171 134 165 255, .rgba 129 139 165 255, .rgba 141 147 164 255, .rgba 167 138 141 255), + (.rgba 65 157 195 255, .rgba 132 152 194 255, .rgba 119 144 195 255, .rgba 59 158 186 255), + (.rgba 98 117 255 255, .rgba 0 124 254 255, .rgba 0 134 254 255, .rgba 34 141 169 255), + (.rgba 206 251 97 255, .rgba 254 242 95 255, .rgba 254 229 102 255, .rgba 225 236 242 255), + (.rgba 175 243 166 255, .rgba 254 234 165 255, .rgba 237 220 168 255, .rgba 192 232 249 255), + (.rgba 215 176 180 255, .rgba 180 180 180 255, .rgba 190 187 179 255, .rgba 214 176 179 255), + (.rgba 99 224 34 255, .rgba 244 210 28 255, .rgba 218 189 51 255, .rgba 140 207 231 255), + (.rgba 148 184 216 255, .rgba 167 182 215 255, .rgba 162 179 216 255, .rgba 144 186 203 255), + (.rgba 134 96 79 255, .rgba 107 100 79 255, .rgba 115 106 77 255, .rgba 135 93 97 255), + (.rgba 108 124 184 255, .rgba 92 125 184 255, .rgba 96 127 183 255, .rgba 95 132 146 255), + (.rgba 227 18 239 255, .rgba 0 96 239 255, .rgba 82 145 236 255, .rgba 210 94 111 255), + (.rgba 136 91 172 255, .rgba 47 101 172 255, .rgba 82 114 171 255, .rgba 123 106 107 255), + (.rgba 146 65 82 255, .rgba 78 79 82 255, .rgba 101 95 79 255, .rgba 145 65 77 255), + (.rgba 184 152 129 255, .rgba 163 154 129 255, .rgba 169 159 128 255, .rgba 186 148 152 255), + (.rgba 86 194 100 255, .rgba 206 183 99 255, .rgba 184 166 104 255, .rgba 116 181 204 255), + (.rgba 84 227 67 255, .rgba 245 213 64 255, .rgba 217 190 77 255, .rgba 131 210 237 255), + (.rgba 58 182 159 255, .rgba 178 173 158 255, .rgba 157 158 160 255, .rgba 83 175 203 255), + (.rgba 12 21 96 255, .rgba 0 27 96 255, .rgba 0 34 95 255, .rgba 0 38 52 255), + (.rgba 213 102 201 255, .rgba 74 125 201 255, .rgba 129 152 198 255, .rgba 203 120 130 255), + (.rgba 81 61 202 255, .rgba 0 75 202 255, .rgba 0 92 201 255, .rgba 20 94 112 255), + (.rgba 224 20 14 255, .rgba 95 81 21 255, .rgba 144 122 0 255, .rgba 225 0 71 255), + (.rgba 171 86 146 255, .rgba 78 102 146 255, .rgba 112 121 144 255, .rgba 165 95 104 255), + (.rgba 38 220 115 255, .rgba 231 206 113 255, .rgba 202 184 120 255, .rgba 103 205 237 255), +] + +/-- The largest per-channel difference between two colors (ignoring alpha). -/ +private def chanMaxDiff : Color → Color → Nat + | .rgba r1 g1 b1 _, .rgba r2 g2 b2 _ => + let d (x y : UInt8) : Nat := (Int.ofNat x.toNat - Int.ofNat y.toNat).natAbs + max (d r1 r2) <| max (d g1 g2) (d b1 b2) + +/-- +The greatest per-channel deviation of `dichromacy` from the DaltonLens reference, over all vectors +and all three deficiencies. Pinned so a regression (or a larger deviation than the matrix rounding +explains) fails the test. +-/ +def cvdReferenceMaxDeviation : Nat := + cvdReferenceVectors.foldl (init := 0) fun acc (c, p, de, t) => + max acc <| + max (chanMaxDiff (dichromacy .protanopia c) p) <| + max (chanMaxDiff (dichromacy .deuteranopia c) de) (chanMaxDiff (dichromacy .tritanopia c) t) + +-- `dichromacy` matches the DaltonLens reference across all 50 vectors and all three deficiencies. The +-- largest per-channel deviation is 7, for one tritanopia color (`rgba 81 61 202`) that sits near the +-- half-plane boundary, where the hard plane switch and the 5-decimal-rounded matrices interact; the +-- rest are within about 3. A transposed matrix, flipped half-plane sign, or wrong gamma direction +-- would push this far higher. +/-- info: 7 -/ +#guard_msgs in +#eval cvdReferenceMaxDeviation + +/-! ## CIEDE2000 against Sharma's published Lab vectors + +`deltaE2000` (the CIELAB core of `deltaE`, reached via `import all`) is validated against the 34 +test pairs from Sharma, Wu & Dalal (2005), Table 1, the canonical data for checking a CIEDE2000 +implementation. These pairs deliberately exercise the hue-rotation and near-zero-chroma cases that +catch transcription errors the broad invariants miss. Values via the reference implementation at +https://github.com/gfiumara/CIEDE2000. +-/ + +def sharmaDeltaEVectors : List ((Float × Float × Float) × (Float × Float × Float) × Float) := [ + ((50.0, 2.6772, -79.7751), (50.0, 0.0, -82.7485), 2.0425), + ((50.0, 3.1571, -77.2803), (50.0, 0.0, -82.7485), 2.8615), + ((50.0, 2.8361, -74.0200), (50.0, 0.0, -82.7485), 3.4412), + ((50.0, -1.3802, -84.2814), (50.0, 0.0, -82.7485), 1.0000), + ((50.0, -1.1848, -84.8006), (50.0, 0.0, -82.7485), 1.0000), + ((50.0, -0.9009, -85.5211), (50.0, 0.0, -82.7485), 1.0000), + ((50.0, 0.0, 0.0), (50.0, -1.0, 2.0), 2.3669), + ((50.0, -1.0, 2.0), (50.0, 0.0, 0.0), 2.3669), + ((50.0, 2.4900, -0.0010), (50.0, -2.4900, 0.0009), 7.1792), + ((50.0, 2.4900, -0.0010), (50.0, -2.4900, 0.0010), 7.1792), + ((50.0, 2.4900, -0.0010), (50.0, -2.4900, 0.0011), 7.2195), + ((50.0, 2.4900, -0.0010), (50.0, -2.4900, 0.0012), 7.2195), + ((50.0, -0.0010, 2.4900), (50.0, 0.0009, -2.4900), 4.8045), + ((50.0, -0.0010, 2.4900), (50.0, 0.0010, -2.4900), 4.8045), + ((50.0, -0.0010, 2.4900), (50.0, 0.0011, -2.4900), 4.7461), + ((50.0, 2.5000, 0.0), (50.0, 0.0, -2.5000), 4.3065), + ((50.0, 2.5000, 0.0), (73.0, 25.0, -18.0), 27.1492), + ((50.0, 2.5000, 0.0), (61.0, -5.0, 29.0), 22.8977), + ((50.0, 2.5000, 0.0), (56.0, -27.0, -3.0), 31.9030), + ((50.0, 2.5000, 0.0), (58.0, 24.0, 15.0), 19.4535), + ((50.0, 2.5000, 0.0), (50.0, 3.1736, 0.5854), 1.0000), + ((50.0, 2.5000, 0.0), (50.0, 3.2972, 0.0), 1.0000), + ((50.0, 2.5000, 0.0), (50.0, 1.8634, 0.5757), 1.0000), + ((50.0, 2.5000, 0.0), (50.0, 3.2592, 0.3350), 1.0000), + ((60.2574, -34.0099, 36.2677), (60.4626, -34.1751, 39.4387), 1.2644), + ((63.0109, -31.0961, -5.8663), (62.8187, -29.7946, -4.0864), 1.2630), + ((61.2901, 3.7196, -5.3901), (61.4292, 2.2480, -4.9620), 1.8731), + ((35.0831, -44.1164, 3.7933), (35.0232, -40.0716, 1.5901), 1.8645), + ((22.7233, 20.0904, -46.6940), (23.0331, 14.9730, -42.5619), 2.0373), + ((36.4612, 47.8580, 18.3852), (36.2715, 50.5065, 21.2231), 1.4146), + ((90.8027, -2.0831, 1.4410), (91.1528, -1.6435, 0.0447), 1.4441), + ((90.9257, -0.5406, -0.9208), (88.6381, -0.8985, -0.7239), 1.5381), + ((6.7747, -0.2908, -2.4247), (5.8714, -0.0985, -2.2286), 0.6377), + ((2.0776, 0.0795, -1.1350), (0.9033, -0.0636, -0.5514), 0.9082), +] + +/-- +The greatest absolute deviation of `deltaE2000` from Sharma's published ΔE₀₀, over all 34 vectors. +Sharma publishes four decimal places, so a correct implementation lands within rounding. +-/ +def sharmaMaxDeviation : Float := + sharmaDeltaEVectors.foldl (init := 0.0) fun acc (lab1, lab2, exp) => + let (l1, a1, b1) := lab1 + let (l2, a2, b2) := lab2 + let d := (deltaE2000 l1 a1 b1 l2 a2 b2 - exp).abs + if acc < d then d else acc + +-- `deltaE2000` reproduces every Sharma reference value to within their published precision (four +-- decimals), confirming the CIEDE2000 formula is transcribed correctly (including the tricky +-- hue-rotation and near-zero-chroma cases). +/-- info: true -/ +#guard_msgs in +#eval sharmaMaxDeviation < 0.0001 diff --git a/src/tests/Tests/Font.lean b/src/tests/Tests/Font.lean new file mode 100644 index 000000000..8fbe66e1d --- /dev/null +++ b/src/tests/Tests/Font.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Verso.Font +import Verso.Theme.Code +import Verso.Theme.Code.Defaults + +/-! +Compile-time tests for `Verso.Font`: the `define_font_face` command embeds file bytes, `Weight` +literals clamp into range, and `Typeface.cssFamily` renders (and escapes) as expected. There is no +general font file to bundle yet, so an existing KaTeX font stands in for the embedding test. +-/ + +open Verso + +-- `define_font_face` embeds the file's bytes at compile time. +define_font_face katexMono where + format := .woff2 + file := "../../../vendored-js/katex/fonts/KaTeX_Typewriter-Regular.woff2" + +/-- info: true -/ +#guard_msgs in #eval katexMono.bytes.size > 1000 +/-- info: Verso.FontFormat.woff2 -/ +#guard_msgs in #eval katexMono.format +/-- info: Verso.FontStyle.normal -/ +#guard_msgs in #eval katexMono.style + +-- `weight :=` is sugar for `weights := .fixed _`; `style` and the file format are honored. +define_font_face boldItalicFace where + weight := .bold + style := .italic + format := .ttf + file := "../../../vendored-js/katex/fonts/KaTeX_Typewriter-Regular.ttf" + +/-- info: some 700 -/ +#guard_msgs in +#eval match boldItalicFace.weights with + | .fixed w => some w.val + | _ => none +/-- info: true -/ +#guard_msgs in #eval boldItalicFace.style = .italic + +-- Named weights and the clamping `OfNat`. +/-- info: 400 -/ +#guard_msgs in #eval Weight.regular.val +/-- info: 600 -/ +#guard_msgs in #eval Weight.semibold.val +/-- info: 1000 -/ +#guard_msgs in #eval (1500 : Weight).val +/-- info: 1 -/ +#guard_msgs in #eval (0 : Weight).val + +-- Default typefaces expand to system stacks; a custom family is quoted and escaped. +/-- info: "ui-sans-serif, system-ui, sans-serif" -/ +#guard_msgs in #eval Typeface.sans.cssFamily +/-- info: "\"Fancy\"" -/ +#guard_msgs in #eval (Typeface.files "Fancy" #[]).cssFamily +/-- info: "\"a\\\"b\"" -/ +#guard_msgs in #eval (Typeface.files "a\"b" #[]).cssFamily + +-- A missing required field is an error. +/-- error: `define_font_face` requires a `format` field -/ +#guard_msgs in +define_font_face noFormat where + file := "x.woff2" + +/-- error: `define_font_face` requires a `file` field -/ +#guard_msgs in +define_font_face noFile where + format := .ttf + +-- `slugFamily` keeps a usable hyphen-separated tail and falls back to "font" for empty input. +/-- info: "Source-Sans-3" -/ +#guard_msgs in #eval Verso.Theme.CodeTheme.slugFamily "Source Sans 3" +/-- info: "Fira-Mono" -/ +#guard_msgs in #eval Verso.Theme.CodeTheme.slugFamily "Fira/Mono" +/-- info: "font" -/ +#guard_msgs in #eval Verso.Theme.CodeTheme.slugFamily "///" + +-- Two distinct families that slug to the same string get distinct asset paths via the typeface +-- index, so one font's bytes can never overwrite the other. +def collidingTheme : Verso.Theme.CodeTheme := { + Verso.Theme.CodeTheme.ink with + codeFace := .files "A B" #[katexMono], + const := { color := color%#000000, weight := .regular, style := .normal, + face := .files "A/B" #[katexMono] } +} + +/-- info: #["assets/fonts/A-B-0-0.woff2", "assets/fonts/A-B-1-0.woff2"] -/ +#guard_msgs in #eval (collidingTheme.fontAssets "assets").map (·.1) diff --git a/src/tests/Tests/HighlightedToTeX.lean b/src/tests/Tests/HighlightedToTeX.lean index dba4aa078..a526d34eb 100644 --- a/src/tests/Tests/HighlightedToTeX.lean +++ b/src/tests/Tests/HighlightedToTeX.lean @@ -5,6 +5,11 @@ Author: Jason Reed -/ module meta import all Verso.Code.HighlightedToTex +public import Verso.Theme.Code +public import Verso.Theme.Code.Defaults +public import Verso.Font +meta import all Verso.Theme.Code +meta import all Verso.Theme.Code.Defaults open Verso.Doc.TeX (escapeForVerbatim) open SubVerso.Highlighting @@ -12,3 +17,63 @@ open SubVerso.Highlighting /-- info: "\\symbol{123}\\symbol{124}\\symbol{125}\\symbol{92}" -/ #guard_msgs in #eval escapeForVerbatim "{|}\\" + +/-! Token rendering wraps each semantic category in a `\verso…` macro. The four categories cover +keywords, constants (including anonymous constructors and options), variables, and a catch-all +literal bucket. -/ + +/-- info: "\\versoKeyword{def}" -/ +#guard_msgs in #eval (highlightToken "def" (.keyword none none "")).asString + +/-- info: "\\versoConst{foo}" -/ +#guard_msgs in #eval (highlightToken "foo" (.const `foo "" none false none)).asString + +/-- info: "\\versoVar{x}" -/ +#guard_msgs in #eval (highlightToken "x" (.var ⟨`x⟩ "" none)).asString + +/-- info: "\\versoLiteral{42}" -/ +#guard_msgs in #eval (highlightToken "42" .unknown).asString + +/-! The fallback macro block defines the four `\verso…` macros with `\providecommand`, so a +preamble that defines its own (theme-driven) versions wins without an explicit `\renewcommand`. -/ + +/-- +info: "\\providecommand{\\versoKeyword}[1]{\\textbf{#1}}\n\\providecommand{\\versoConst}[1]{#1}\n\\providecommand{\\versoVar}[1]{\\textit{#1}}\n\\providecommand{\\versoLiteral}[1]{#1}\n\\providecommand{\\versoLiteralString}[1]{#1}\n\\providecommand{\\versoDocComment}[1]{\\textit{#1}}\n\\providecommand{\\versoSort}[1]{#1}\n\\providecommand{\\versoLevelVar}[1]{\\textit{#1}}\n\\providecommand{\\versoLevelConst}[1]{#1}\n\\providecommand{\\versoLevelOp}[1]{#1}\n\\providecommand{\\versoModuleName}[1]{#1}\n\\providecommand{\\versoDelim}[1]{#1}\n\\providecommand{\\versoOperator}[1]{#1}\n\\providecommand{\\versoBracket}[1]{#1}\n\\providecommand{\\versoSeparator}[1]{#1}\n\\providecommand{\\versoLiteralNumber}[1]{#1}\n\\providecommand{\\versoLiteralChar}[1]{#1}\n\\providecommand{\\versoComment}[1]{#1}\n\\providecommand{\\versoCommentDelim}[1]{#1}\n" +-/ +#guard_msgs in #eval texMacroFallbacks + +/-! The default code theme emits `\definecolor` blocks for its token and severity colors and +redefines each `\verso…` macro to apply the resolved color, weight, and style. -/ + +private def hasSub (s sub : String) : Bool := s.any sub + +/-- info: true -/ +#guard_msgs in +#eval + let p := Verso.Theme.CodeTheme.ink.texPreamble + -- Message-text and accent colors are emitted under distinct names: `errorColor` is the + -- message-body color (#cc0000 by default), `errorIndicatorColor` is the wavy-underline + -- accent (#ff0000). The keyword macro picks up bold (NFSS `eb`), and the mono font is + -- the bundled DejaVu Sans Mono. + hasSub p "\\definecolor{errorColor}{HTML}{CC0000}" && + hasSub p "\\definecolor{errorIndicatorColor}{HTML}{FF0000}" && + hasSub p "\\renewcommand{\\versoKeyword}[1]{\\textcolor{versoKeywordColor}{\\fontseries{eb}\\fontshape{n}\\selectfont #1}}" && + hasSub p "\\setmonofont{DejaVu Sans Mono}" + +/-! A deliberately colorful theme really does color and style the keyword and const tokens. -/ + +open Verso Verso.Theme in +private def colorfulTheme : CodeTheme := { + CodeTheme.ink with + keyword := { color := color%#aa3300, weight := 600, style := .normal, face := .mono }, + const := { color := color%#0044bb, weight := .regular, style := .italic, face := .mono } +} + +/-- info: true -/ +#guard_msgs in +#eval + let p := colorfulTheme.texPreamble + hasSub p "\\definecolor{versoKeywordColor}{HTML}{AA3300}" && + hasSub p "\\renewcommand{\\versoKeyword}[1]{\\textcolor{versoKeywordColor}{\\fontseries{b}\\fontshape{n}\\selectfont #1}}" && + hasSub p "\\definecolor{versoConstColor}{HTML}{0044BB}" && + hasSub p "\\renewcommand{\\versoConst}[1]{\\textcolor{versoConstColor}{\\fontseries{m}\\fontshape{it}\\selectfont #1}}" diff --git a/src/tests/Tests/TexUtil.lean b/src/tests/Tests/TexUtil.lean index 43e0a1570..5b74efa45 100644 --- a/src/tests/Tests/TexUtil.lean +++ b/src/tests/Tests/TexUtil.lean @@ -39,4 +39,4 @@ def toTex (block : Doc.Block Genre.Manual) : IO Output.TeX := do -- Convert the block to TeX block.toTeX |>.run ⟨options, traverseContext, traverseState, {}⟩ - |>.run' {} |>.run extension_impls |>.run logger + |>.run' {} |>.run ({} : Theme.ThemeRegistry) |>.run extension_impls |>.run logger diff --git a/src/tests/ThemeTestDoc.lean b/src/tests/ThemeTestDoc.lean new file mode 100644 index 000000000..9fbfedf64 --- /dev/null +++ b/src/tests/ThemeTestDoc.lean @@ -0,0 +1,41 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean + +set_option pp.rawOnError true + +#doc (Manual) "Theme test" => + +# Code samples + +A line of prose with an [external content link](https://example.com/) that the browser test +checks against the theme's `linkColor`. Then code that mixes a keyword, a const, and a literal. + +```lean +def hello (name : String) : String := s!"hello, {name}" +``` + +# Diagnostics + +A block that errors, so the rendered HTML carries the `.lean-output.error` rule used by the +theme's error indicator color: + +```lean +error (name := badProof) +example : 2 + 2 = 5 := by rfl +``` + +```leanOutput badProof +Tactic `rfl` failed: The left-hand side + 2 + 2 +is not definitionally equal to the right-hand side + 5 + +⊢ 2 + 2 = 5 +``` diff --git a/src/tests/ThemeTestMain.lean b/src/tests/ThemeTestMain.lean new file mode 100644 index 000000000..14bbeb5c0 --- /dev/null +++ b/src/tests/ThemeTestMain.lean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import Verso +import VersoManual +import ThemeTestDoc + +open Verso Verso.Theme +open Verso.Genre Manual + +/-! +The customized {name}`Verso.Theme.CodeTheme` used by the browser test. Each color field +holds a distinct sentinel hex value so Playwright can identify which theme field a rendered DOM +color comes from. +-/ +def testTheme : CodeTheme := { + name := "ThemeTest", + appearance := .light, + background := color%#000101, + codeBlockBackground := color%#000202, + textColor := color%#000303, + codeColor := color%#000404, + structureColor := color%#000505, + selectedColor := color%#000606, + infoColor := color%#000707, + infoIndicatorColor := color%#000808, + warningColor := color%#000909, + warningIndicatorColor := color%#000a0a, + errorColor := color%#000b0b, + errorIndicatorColor := color%#000c0c, + hoverBackground := color%#000d0d, + hoverBorderColor := color%#000e0e, + hoverText := color%#000f0f, + hoverSeparatorColor := color%#001010, + tokenHighlightBackground := color%#001111, + tacticStateBackground := color%#001212, + tacticStateBorderColor := color%#001313, + highlightOnCode := color%#001414, + highlightOnText := color%#001515, + uiOnCode := color%#001616, + const := { color := color%#001717, weight := 500, style := .italic, face := .sans }, + keyword := { color := color%#001818, weight := 800, style := .italic, face := .serif }, + «var» := { color := color%#001919, weight := 300, style := .normal, face := .mono }, +} + +def config : Config where + emitTeX := false + emitHtmlSingle := .no + emitHtmlMulti := .immediately + htmlDepth := 1 + +@[manual_theme] +def testManualTheme : ManualTheme := { + ManualTheme.ink with + toCodeTheme := testTheme, + surfaceColor := color%#001a1a, + headerBackground := color%#001b1b, + tocBackground := color%#001c1c, + borderColor := color%#001d1d, + mutedColor := color%#001e1e, + highlightColor := color%#001f1f, + linkColor := color%#002020, + visitedLinkColor := color%#002121, + tocTextColor := color%#002222, + burgerVisibleColor := color%#002323, + burgerVisibleShadowColor := color%#002424, + burgerHiddenColor := color%#002525, + burgerHiddenShadowColor := color%#002626 +} + +/-- +Dark counterpart to `testManualTheme`. The validation pass requires a registered dark theme +for `defaultDarkTheme`, but the browser test only inspects the unscoped `:root` block (the light +default in the default follow-system mode), so the same sentinel palette under `.dark` is fine. +-/ +@[manual_theme] +def testManualThemeDark : ManualTheme := { + testManualTheme with + toCodeTheme := { testTheme with name := "ThemeTest Dark", appearance := .dark } +} + +/-! +Unit checks for the no-JavaScript / picker scaffolding driven by {name}`Verso.Theme.ThemeMode`. A +two-theme registry (one light, one dark) stands in for a real build's available set. The report +below records, per generated output, whether the mode-dependent content is present. + +Follow-system mode pairs a light `:root` with a `prefers-color-scheme: dark` media block; light and +dark mode emit a single `:root` with no media swap. The configured mode must also reach the +no-flash script (as `DEFAULT_MODE`) and the picker's `window.versoThemes` data file. +-/ +private def modeCheckRegistry : ThemeRegistry := + (({} : ThemeRegistry).insert `light ManualTheme.ink).insert `dark ManualTheme.argent + +private def hasSubstr (haystack needle : String) : Bool := + (haystack.splitOn needle).length > 1 + +/-- +info: css @media(dark) by mode -> followSystem=true light=false dark=false +themeInitScript inlines the configured mode: true +windowVersoThemesJs carries the configured mode: true +-/ +#guard_msgs in +#eval do + let mediaFor (m : ThemeMode) : Bool := + hasSubstr («verso-themes.css» modeCheckRegistry `light `dark m) "@media (prefers-color-scheme: dark)" + IO.println s!"css @media(dark) by mode -> followSystem={mediaFor .followSystem} light={mediaFor .light} dark={mediaFor .dark}" + IO.println s!"themeInitScript inlines the configured mode: {hasSubstr (themeInitScript modeCheckRegistry `light `dark .dark) "var DEFAULT_MODE = \"dark\""}" + IO.println s!"windowVersoThemesJs carries the configured mode: {hasSubstr (windowVersoThemesJs modeCheckRegistry `light `dark .light "sample") "\"defaultMode\":\"light\""}" + +def main : List String → IO UInt32 := + manualMain (%doc ThemeTestDoc) + (config := { config with + defaultLightTheme := ``testManualTheme, + defaultDarkTheme := ``testManualThemeDark, + -- The sentinel palette deliberately violates accessibility; the test exercises rendering, + -- not the accessibility checks. + strictThemeCoverage := false, + strictDefaultThemeAccessibility := false, + warnPerThemeAccessibility := false }) diff --git a/src/tests/golden/.gitignore b/src/tests/golden/.gitignore new file mode 100644 index 000000000..7de0b67ed --- /dev/null +++ b/src/tests/golden/.gitignore @@ -0,0 +1 @@ +*.output diff --git a/src/tests/golden/theme-css/default.expected b/src/tests/golden/theme-css/default.expected new file mode 100644 index 000000000..22eb43b0f --- /dev/null +++ b/src/tests/golden/theme-css/default.expected @@ -0,0 +1,896 @@ +:root { + --verso-background-color: #ffffff; + --verso-code-background-color: #ffffff; + --verso-text-color: #000000; + --verso-code-color: #000000; + --verso-structure-color: #000000; + --verso-selected-color: #ddeeff; + --verso-info-color: #000000; + --verso-info-indicator-color: #4777ff; + --verso-warning-color: #000000; + --verso-warning-indicator-color: #d97706; + --verso-error-color: #cc0000; + --verso-error-indicator-color: #ff0000; + --verso-code-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-const-color: #000000; + --verso-code-const-weight: 400; + --verso-code-const-style: normal; + --verso-code-const-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-keyword-color: #000000; + --verso-code-keyword-weight: 700; + --verso-code-keyword-style: normal; + --verso-code-keyword-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-var-color: #000000; + --verso-code-var-weight: 400; + --verso-code-var-style: italic; + --verso-code-var-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-literal-color: #000000; + --verso-code-literal-weight: 400; + --verso-code-literal-style: normal; + --verso-code-literal-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-literal-string-color: #000000; + --verso-code-literal-string-weight: 400; + --verso-code-literal-string-style: normal; + --verso-code-literal-string-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-literal-number-color: #000000; + --verso-code-literal-number-weight: 400; + --verso-code-literal-number-style: normal; + --verso-code-literal-number-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-literal-char-color: #000000; + --verso-code-literal-char-weight: 400; + --verso-code-literal-char-style: normal; + --verso-code-literal-char-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-doc-comment-color: #000000; + --verso-code-doc-comment-weight: 400; + --verso-code-doc-comment-style: italic; + --verso-code-doc-comment-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-comment-color: #000000; + --verso-code-comment-weight: 400; + --verso-code-comment-style: normal; + --verso-code-comment-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-comment-delim-color: #000000; + --verso-code-comment-delim-weight: 400; + --verso-code-comment-delim-style: normal; + --verso-code-comment-delim-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-sort-color: #000000; + --verso-code-sort-weight: 400; + --verso-code-sort-style: normal; + --verso-code-sort-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-level-var-color: #000000; + --verso-code-level-var-weight: 400; + --verso-code-level-var-style: italic; + --verso-code-level-var-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-level-const-color: #000000; + --verso-code-level-const-weight: 400; + --verso-code-level-const-style: normal; + --verso-code-level-const-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-level-op-color: #000000; + --verso-code-level-op-weight: 400; + --verso-code-level-op-style: normal; + --verso-code-level-op-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-module-name-color: #000000; + --verso-code-module-name-weight: 400; + --verso-code-module-name-style: normal; + --verso-code-module-name-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-delim-color: #000000; + --verso-code-delim-weight: 400; + --verso-code-delim-style: normal; + --verso-code-delim-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-operator-color: #000000; + --verso-code-operator-weight: 400; + --verso-code-operator-style: normal; + --verso-code-operator-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-bracket-color: #000000; + --verso-code-bracket-weight: 400; + --verso-code-bracket-style: normal; + --verso-code-bracket-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-code-separator-color: #000000; + --verso-code-separator-weight: 400; + --verso-code-separator-style: normal; + --verso-code-separator-font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + --verso-hover-background-color: #e5e5e5; + --verso-hover-border-color: #000000; + --verso-hover-text-color: #000000; + --verso-hover-separator-color: #cccccc; + --verso-token-highlight-background-color: #eeeeee; + --verso-tactic-state-background-color: #ffffff; + --verso-tactic-state-border-color: #888888; + --verso-highlight-on-code-color: #fff3b0; + --verso-highlight-on-text-color: #fff3b0; + --verso-ui-on-code-color: #888888; +} + + + +.hl.lean { + white-space: pre; + font-weight: normal; + font-style: normal; + font-size: inherit; +} + +.hl.lean .keyword { + color: var(--verso-code-keyword-color,); + font-weight: var(--verso-code-keyword-weight, bold); + font-style: var(--verso-code-keyword-style, normal); + font-family: var(--verso-code-keyword-font-family,); +} + +.hl.lean .const { + color: var(--verso-code-const-color,); + font-weight: var(--verso-code-const-weight, normal); + font-style: var(--verso-code-const-style, normal); + font-family: var(--verso-code-const-font-family,); +} + +.hl.lean .var { + color: var(--verso-code-var-color,); + font-weight: var(--verso-code-var-weight, normal); + font-style: var(--verso-code-var-style, italic); + font-family: var(--verso-code-var-font-family,); + + position: relative; +} + +.hl.lean .unknown { + color: var(--verso-code-color,); + font-weight: normal; + font-style: normal; + font-family: var(--verso-code-font-family,); +} + +.hl.lean .literal { + color: var(--verso-code-literal-color, var(--verso-code-color,)); + font-weight: var(--verso-code-literal-weight, normal); + font-style: var(--verso-code-literal-style, normal); + font-family: var(--verso-code-literal-font-family, var(--verso-code-font-family,)); +} + +/* `.literal.string` is more specific than `.literal`, so its rule wins when both classes + apply (string literals). Other future `.literal.*` kinds will fall back to the `.literal` + rule above until they get their own variables. */ +.hl.lean .literal.string { + color: var(--verso-code-literal-string-color, var(--verso-code-literal-color, var(--verso-code-color,))); + font-weight: var(--verso-code-literal-string-weight, normal); + font-style: var(--verso-code-literal-string-style, normal); + font-family: var(--verso-code-literal-string-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .doc-comment { + color: var(--verso-code-doc-comment-color, var(--verso-code-color,)); + font-weight: var(--verso-code-doc-comment-weight, normal); + font-style: var(--verso-code-doc-comment-style, italic); + font-family: var(--verso-code-doc-comment-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .sort { + color: var(--verso-code-sort-color, var(--verso-code-color,)); + font-weight: var(--verso-code-sort-weight, normal); + font-style: var(--verso-code-sort-style, normal); + font-family: var(--verso-code-sort-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .level-var { + color: var(--verso-code-level-var-color, var(--verso-code-color,)); + font-weight: var(--verso-code-level-var-weight, normal); + font-style: var(--verso-code-level-var-style, italic); + font-family: var(--verso-code-level-var-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .level-const { + color: var(--verso-code-level-const-color, var(--verso-code-color,)); + font-weight: var(--verso-code-level-const-weight, normal); + font-style: var(--verso-code-level-const-style, normal); + font-family: var(--verso-code-level-const-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .level-op { + color: var(--verso-code-level-op-color, var(--verso-code-color,)); + font-weight: var(--verso-code-level-op-weight, normal); + font-style: var(--verso-code-level-op-style, normal); + font-family: var(--verso-code-level-op-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .module-name { + color: var(--verso-code-module-name-color, var(--verso-code-color,)); + font-weight: var(--verso-code-module-name-weight, normal); + font-style: var(--verso-code-module-name-style, normal); + font-family: var(--verso-code-module-name-font-family, var(--verso-code-font-family,)); +} + +/* `.anon-ctor` (anonymous-constructor brackets) and `.wildcard` (`_` holes) default to the + unthemed `.unknown` appearance — neither has its own theme bucket yet. `.anon-ctor` also + carries the `.const` class, so the themeable `.const` rule above wins for it where set. + Number, character, and comment kinds are themed via their own rules further down. */ +.hl.lean .anon-ctor, +.hl.lean .wildcard { + color: var(--verso-code-color,); + font-weight: normal; + font-style: normal; + font-family: var(--verso-code-font-family,); +} + +.hl.lean .literal.number { + color: var(--verso-code-literal-number-color, var(--verso-code-literal-color, var(--verso-code-color,))); + font-weight: var(--verso-code-literal-number-weight, normal); + font-style: var(--verso-code-literal-number-style, normal); + font-family: var(--verso-code-literal-number-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .literal.char { + color: var(--verso-code-literal-char-color, var(--verso-code-literal-string-color, var(--verso-code-literal-color, var(--verso-code-color,)))); + font-weight: var(--verso-code-literal-char-weight, normal); + font-style: var(--verso-code-literal-char-style, normal); + font-family: var(--verso-code-literal-char-font-family, var(--verso-code-font-family,)); +} + +/* `.comment` covers line and block comments (their elements carry `comment line` and + `comment block` class pairs respectively); `.comment.delimiter` is a more specific + override for the `--` / `/-` / `-/` punctuation. The themeable `.doc-comment` rule above + wins for doc comments since SubVerso tags them with their own class entirely. */ +.hl.lean .comment { + color: var(--verso-code-comment-color, var(--verso-code-color,)); + font-weight: var(--verso-code-comment-weight, normal); + font-style: var(--verso-code-comment-style, normal); + font-family: var(--verso-code-comment-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .comment.delimiter { + color: var(--verso-code-comment-delim-color, var(--verso-code-comment-color, var(--verso-code-color,))); + font-weight: var(--verso-code-comment-delim-weight, normal); + font-style: var(--verso-code-comment-delim-style, normal); + font-family: var(--verso-code-comment-delim-font-family, var(--verso-code-font-family,)); +} + +/* `.delim` is the built-in syntactic delimiter family (`:=`, `=>`, `←`, `@`, `:`, `|`). The + three punctuation buckets — `.punctuation.operator`, `.punctuation.bracket`, + `.punctuation.separator` — are themed independently below; their CSS variables resolve + per-theme to either the cascade default (delim's color) or an explicit override. */ +.hl.lean .delim { + color: var(--verso-code-delim-color, var(--verso-code-color,)); + font-weight: var(--verso-code-delim-weight, normal); + font-style: var(--verso-code-delim-style, normal); + font-family: var(--verso-code-delim-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .punctuation.operator { + color: var(--verso-code-operator-color, var(--verso-code-color,)); + font-weight: var(--verso-code-operator-weight, normal); + font-style: var(--verso-code-operator-style, normal); + font-family: var(--verso-code-operator-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .punctuation.bracket { + color: var(--verso-code-bracket-color, var(--verso-code-color,)); + font-weight: var(--verso-code-bracket-weight, normal); + font-style: var(--verso-code-bracket-style, normal); + font-family: var(--verso-code-bracket-font-family, var(--verso-code-font-family,)); +} + +.hl.lean .punctuation.separator { + color: var(--verso-code-separator-color, var(--verso-code-color,)); + font-weight: var(--verso-code-separator-weight, normal); + font-style: var(--verso-code-separator-style, normal); + font-family: var(--verso-code-separator-font-family, var(--verso-code-font-family,)); +} + + +.hover-container { + width: 0; + height: 0; + position: relative; + display: inline; +} + +.hl.lean a { + color: inherit; + text-decoration: currentcolor underline dotted; +} + +.hl.lean a:hover { + text-decoration: currentcolor underline solid; +} + +.hl.lean .hover-info { + white-space: normal; +} + +.hl.lean .token .hover-info { + display: none; + position: absolute; + background-color: var(--verso-hover-background-color, #e5e5e5); + border: 1px solid var(--verso-hover-border-color, black); + padding: 0.5rem; + z-index: 300; +} + +.hl.lean .hover-info.messages { + max-height: 10rem; + overflow-y: auto; + overflow-x: hidden; + scrollbar-gutter: stable; + padding: 0 0.5rem 0 0; + display: block; +} + +.hl.lean .hover-info code { + white-space: pre-wrap; + background: none; + color: var(--verso-hover-text-color, black); +} + +.hl.lean .hover-info.messages > code { + padding: 0.5rem; + display: block; + width: fit-content; +} + +.hl.lean .hover-info.messages > code:only-child { + margin: 0; +} + +.hl.lean .hover-info.messages > code { + margin: 0.1rem; +} + +.hl.lean .hover-info.messages > code:not(:first-child) { + margin-top: 0rem; +} + +.hl.lean { +} + +.hl.lean.block { + display: block; +} + +.hl.lean.inline { + display: inline; + white-space: pre-wrap; +} + +.hl.lean * { +} + +.hl.lean .token { + transition: all 0.25s; /* Slight fade for highlights */ +} + +@media (hover: hover) { + .hl.lean .token.binding-hl, .hl.lean .literal:hover, .hl.lean .token.typed:hover { + background-color: var(--verso-token-highlight-background-color, #eeeeee); + border-radius: 2px; + transition: none; + } +} + + +.hl.lean .has-info .token:not(.tactic-state):not(.tactic-state *), .hl.lean .has-info .inter-text:not(.tactic-state):not(.tactic-state *) { + text-decoration-style: wavy; + text-decoration-line: underline; + text-decoration-thickness: from-font; + text-decoration-skip-ink: none; +} + +.hl.lean .has-info .hover-info { + display: none; + position: absolute; + transform: translate(0.25rem, 0.3rem); + border: 1px solid var(--verso-hover-border-color, black); + padding: 0.5rem; + z-index: 400; + text-align: left; +} + +.hl.lean .has-info.error :not(.tactic-state):not(.tactic-state *){ + text-decoration-color: var(--verso-error-indicator-color, red); +} + +@media (hover: hover) { + .hl.lean .has-info.error:hover { + background-color: var(--verso-token-highlight-background-color, #eeeeee); + } +} + +.hl.lean .hover-info.messages > code.error { + background-color: var(--verso-hover-background-color, #e5e5e5); + border-left: 0.2rem solid var(--verso-error-indicator-color, red); +} + +.tippy-box[data-theme~='error'] .hl.lean .hover-info.messages > code.error { + background: none; + border: none; +} + +.error .verso-message, .error .verso-message .token, .error .verso-message label { + color: var(--verso-error-color); +} + +.error .verso-message .case-label:has(input[type="checkbox"])::before { + background-color: var(--verso-error-color) !important; +} + +.hl.lean .has-info.warning :not(.tactic-state):not(.tactic-state *) { + text-decoration-color: var(--verso-warning-indicator-color); +} + +@media (hover: hover) { + .hl.lean .has-info.warning:hover { + background-color: var(--verso-token-highlight-background-color, #eeeeee); + } +} + +.hl.lean .hover-info.messages > code.warning { + background-color: var(--verso-hover-background-color, #e5e5e5); +} + +.lean-output { + border-left: 0.2em solid transparent; + padding: 0 0 0 0.5em; + border-top-left-radius: 0; + border-bottom-left-radius: 0; +} + +.lean-output.error { + border-color: var(--verso-error-indicator-color); +} + +.lean-output.information { + border-color: var(--verso-info-indicator-color); +} + +.lean-output.warning { + border-color: var(--verso-warning-indicator-color); +} + +.tippy-box[data-theme~='warning'] .hl.lean .hover-info.messages > code.warning { + background: none; + border: none; +} + + +.hl.lean .has-info.information :not(.tactic-state):not(.tactic-state *) { + text-decoration-color: var(--verso-info-indicator-color, blue); +} + +@media (hover: hover) { + .hl.lean .has-info.information:hover { + background-color: var(--verso-token-highlight-background-color, #eeeeee); + } +} + + +.hl.lean .hover-info.messages > code.information { + background-color: var(--verso-hover-background-color, #e5e5e5); + border-left: 0.2rem solid var(--verso-info-indicator-color, blue); +} + +.tippy-box[data-theme~='info'] .hl.lean .hover-info.messages > code.information { + background: none; + border: none; +} + +.hl.lean div.docstring { + font-family: var(--verso-text-font-family, sans-serif); + white-space: normal; + max-width: calc(min(40rem, 90vw)); + width: max-content; +} + +.hl.lean div.docstring > :last-child { + margin-bottom: 0; +} + +.hl.lean div.docstring > :first-child { + margin-top: 0; +} + +.hl.lean .hover-info .sep { + display: block; + width: auto; + margin-left: 1rem; + margin-right: 1rem; + margin-top: 0.5rem; + margin-bottom: 0.5rem; + padding: 0; + height: 1px; + border-top: 1px solid var(--verso-hover-separator-color, #cccccc); +} + +.hl.lean code { + font-family: var(--verso-code-font-family); +} + +.hl.lean .tactic-state { + display: none; + position: relative; + width: fit-content; + border: 1px solid var(--verso-tactic-state-border-color, #888888); + border-radius: 0.1rem; + padding: 0.5rem; + font-family: sans-serif; + background-color: var(--verso-tactic-state-background-color, #ffffff); +} + +.hl.lean.popup .tactic-state { + position: static; + display: block; + width: auto; + border: none; + padding: 0.5rem; + font-family: sans-serif; + background-color: var(--verso-tactic-state-background-color, #ffffff); +} + + +.hl.lean .tactic { + position: relative; + display: inline; + vertical-align: top; + /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/ + -webkit-text-size-adjust: 100%; + text-size-adjust: 100%; +} + +.hl.lean .tactic:has(> .tactic-toggle:checked) { + display: inline-grid; + grid-template-columns: 1fr; +} + +.hl.lean .tactic-toggle:checked ~ .tactic-state { + display: inline-block; + vertical-align: top; + grid-row: 2; + justify-self: start; +} + +.hl.lean .tactic > label { + position: relative; + grid-row: 1; + display: inline; +} + +@media (hover: hover) { + /* Highlight a region on hover only when its own toggle is unchecked, and only the innermost + hovered region: `label:hover` bubbles to ancestor labels, so suppress the highlight on a region + whose label contains a more deeply nested hovered tactic label. */ + .hl.lean .tactic:has(> .tactic-toggle:not(:checked)) > label:hover:not(:has(.tactic > label:hover)) { + background-color: var(--verso-token-highlight-background-color, #eeeeee); + } +} + +.hl.lean .tactic-toggle { + position: absolute; + top: 0; + left: 0; + opacity: 0; + height: 0; + width: 0; + z-index: -10; +} + +.hl.lean .tactic > label::after { + content: ""; + border: 1px solid var(--verso-ui-on-code-color, #888888); + /* These need to be em, not rem, to scale with the font */ + border-radius: 1em; + height: 0.25em; + vertical-align: middle; + width: 0.6em; + margin-left: 0.1em; + margin-right: 0.1em; + display: inline-block; + transition: all 0.5s; +} + +/* +@media (hover: hover) { + .hl.lean .tactic > label:hover::after { + border: 1px solid #aaaaaa; + background-color: #aaaaaa; + transition: all 0.5s; + } +} +*/ + +.hl.lean .tactic > label:has(+ .tactic-toggle:checked)::after { + border: 1px solid var(--verso-ui-on-code-color, #888888); + background-color: var(--verso-ui-on-code-color, #888888); + transition: all 0.5s; +} + +.hl.lean .tactic-state .goal + .goal { + margin-top: 1.5em; +} + +/* +Some CSS frameworks customize details/summary in ways not compatible with Verso's output. +*/ + +.hl.lean details { + display: block !important; + margin: 0; +} + +.hl.lean details summary { + display: list-item !important; + margin: 0; +} + +.hl.lean details summary:focus { + outline: none; + outline-offset: none; + color: inherit; +} + +.hl.lean ul > li { + margin-bottom: 0; +} + +.hl.lean details summary::marker { + display: inline !important; +} + +.hl.lean details > summary:first-of-type { + list-style-type: disclosure-closed; + list-style-position: inside; +} + +.hl.lean details[open] > summary:first-of-type { + list-style-type: disclosure-open; +} + +.hl.lean details summary::before, .hl.lean details summary::after { + content: "" !important; + background: none; + display: none; +} + +.hl.lean .tactic-state summary { + /* These need to be em, not rem, to scale with the font */ + margin-left: -0.5em; +} + +.hl.lean .tactic-state details { + /* These need to be em, not rem, to scale with the font */ + padding-left: 0.5em; +} + +.hl.lean .case-label { + display: block; + position: relative; +} + +.hl.lean .case-label input[type="checkbox"] { + position: absolute; + top: 0; + left: 0; + opacity: 0; + height: 0; + width: 0; + z-index: -10; +} + +.hl.lean .case-label:has(input[type="checkbox"])::before { + display: inline-block; + background-color: var(--verso-code-color, black); + content: ' '; + transition: ease 0.2s; + margin-right: 0.7em; + clip-path: polygon(100% 0, 0 0, 50% 100%); + width: 0.6em; + height: 0.6em; + vertical-align: middle; +} + +.hl.lean .case-label:has(input[type="checkbox"]:not(:checked))::before { + transform: rotate(-90deg); +} + +.hl.lean .case-label:has(input[type="checkbox"]) { + +} + +.hl.lean .case-label:has(input[type="checkbox"]:checked) { + +} + + +.hl.lean .labeled-case > :not(:first-child) { + max-height: 0px; + display: block; + overflow: hidden; + transition: max-height 0.1s ease-in; + /* These need to be em, not rem, to scale with the font */ + margin-left: 0.5em; + margin-top: 0.1em; +} + +.hl.lean .labeled-case:has(.case-label input[type="checkbox"]:checked) > :not(:first-child) { + max-height: 100%; +} + + +.hl.lean .goal-name::before { + font-style: normal; + content: "case "; +} + +.hl.lean .goal-name { + font-style: italic; + font-family: var(--verso-code-font-family); + color: inherit; +} + +.hl.lean .hypotheses { + display: table; +} + +.hl.lean .hypothesis { + display: table-row; +} + +.hl.lean .hypothesis > * { + display: table-cell; +} + + +.hl.lean .hypotheses .colon { + text-align: center; + /* This needs to be em, not rem, to scale with the font */ + min-width: 1em; +} + +.hl.lean .hypotheses .name { + text-align: right; +} + +.hl.lean .hypotheses .name, +.hl.lean .hypotheses .type, +.hl.lean .conclusion .type { + font-family: var(--verso-code-font-family); +} + +.tippy-box { + /* Without these, mobile Safari will start making font sizes inconsistent when its text size adjustment feature is triggered.*/ + -webkit-text-size-adjust: 100%; + text-size-adjust: 100%; +} + +.tippy-box[data-theme~='lean'] { + background-color: var(--verso-hover-background-color, #e5e5e5); + color: var(--verso-hover-text-color, black); + border: 1px solid var(--verso-hover-border-color, black); +} +.tippy-box[data-theme~='lean'][data-placement^='top'] > .tippy-arrow::before { + border-top-color: var(--verso-hover-background-color, #e5e5e5); +} +.tippy-box[data-theme~='lean'][data-placement^='bottom'] > .tippy-arrow::before { + border-bottom-color: var(--verso-hover-background-color, #e5e5e5); +} +.tippy-box[data-theme~='lean'][data-placement^='left'] > .tippy-arrow::before { + border-left-color: var(--verso-hover-background-color, #e5e5e5); +} +.tippy-box[data-theme~='lean'][data-placement^='right'] > .tippy-arrow::before { + border-right-color: var(--verso-hover-background-color, #e5e5e5); +} + +.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::before { + border-top-color: var(--verso-hover-background-color, #e5e5e5); + border-width: 11px 11px 0; +} +.tippy-box[data-theme~='message'][data-placement^='top'] > .tippy-arrow::after { + bottom: -11px; + border-width: 11px 11px 0; +} +.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::before { + border-width: 0 11px 11px; +} +.tippy-box[data-theme~='message'][data-placement^='bottom'] > .tippy-arrow::after { + top: -11px; + border-width: 0 11px 11px; +} +.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::before { + border-left-color: var(--verso-hover-background-color, #e5e5e5); + border-width: 11px 0 11px 11px; +} +.tippy-box[data-theme~='message'][data-placement^='left'] > .tippy-arrow::after { + right: -11px; + border-width: 11px 0 11px 11px; +} + +.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::before { + border-right-color: var(--verso-hover-background-color, #e5e5e5); + border-width: 11px 11px 11px 0; +} +.tippy-box[data-theme~='message'][data-placement^='right'] > .tippy-arrow::after { + left: -11px; + border-width: 11px 11px 11px 0; +} + + + +.tippy-box[data-theme~='warning'] { + background-color: var(--verso-hover-background-color, #e5e5e5); + color: var(--verso-hover-text-color, black); + border: 3px solid var(--verso-warning-indicator-color, #e7a71d); +} + +.tippy-box[data-theme~='error'] { + background-color: var(--verso-hover-background-color, #e5e5e5); + color: var(--verso-hover-text-color, black); + border: 3px solid var(--verso-error-indicator-color, red); +} + +.tippy-box[data-theme~='info'] { + background-color: var(--verso-hover-background-color, #e5e5e5); + color: var(--verso-hover-text-color, black); + border: 3px solid var(--verso-info-indicator-color, blue); +} + +.tippy-box[data-theme~='tactic'] { + background-color: var(--verso-tactic-state-background-color, #ffffff); + color: var(--verso-hover-text-color, black); + border: 1px solid var(--verso-hover-border-color, black); +} +.tippy-box[data-theme~='tactic'][data-placement^='top'] > .tippy-arrow::before { + border-top-color: var(--verso-tactic-state-background-color, #ffffff); +} +.tippy-box[data-theme~='tactic'][data-placement^='bottom'] > .tippy-arrow::before { + border-bottom-color: var(--verso-tactic-state-background-color, #ffffff); +} +.tippy-box[data-theme~='tactic'][data-placement^='left'] > .tippy-arrow::before { + border-left-color: var(--verso-tactic-state-background-color, #ffffff); +} +.tippy-box[data-theme~='tactic'][data-placement^='right'] > .tippy-arrow::before { + border-right-color: var(--verso-tactic-state-background-color, #ffffff); +} + +.extra-doc-links { + list-style-type: none; + margin-left: 0; + padding: 0; +} + +.extra-doc-links > li { + display: inline-block; +} + +.extra-doc-links > li:not(:last-child)::after { + content: '|'; + display: inline-block; + margin: 0 0.25em; +} + +.verso-message .trace { + display: block; +} + +.verso-message .trace > summary::marker { + color: var(--verso-text-color); +} + +.verso-message .trace-children { + margin: 0; + padding: 0; +} + +.verso-message .trace-children > li { + list-style-type: none; + margin-left: 1.5em; +} + +.verso-message .trace-children > li:not(:has(.trace)) { + margin-left: 0; +} + +.verso-message .trace-class { + color: color-mix(in srgb, currentColor 70%, transparent); + font-weight: bold; + margin: 0; + padding: 0; +} + +.verso-message .text { + white-space: pre-wrap; +} diff --git a/src/tests/golden/theme-css/default.input b/src/tests/golden/theme-css/default.input new file mode 100644 index 000000000..331d858ce --- /dev/null +++ b/src/tests/golden/theme-css/default.input @@ -0,0 +1 @@ +default \ No newline at end of file diff --git a/src/tests/integration/code-content-doc/expected/tex/main.tex b/src/tests/integration/code-content-doc/expected/tex/main.tex index 4d245fe9d..8e2c4c4e9 100644 --- a/src/tests/integration/code-content-doc/expected/tex/main.tex +++ b/src/tests/integration/code-content-doc/expected/tex/main.tex @@ -51,12 +51,11 @@ % Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro \newunicodechar{‑}{-} -\definecolor{errorColor}{HTML}{B91C1C} -\definecolor{infoColor}{HTML}{1E6BB8} -\definecolor{warningColor}{HTML}{D97706} -\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}} -\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}} -\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}} +% Decoration accents (wavy underlines) use the *indicator* colors, distinct from the message +% text colors. The theme block below redefines both. +\newcommand{\errorDecorate}[1]{\coloredwave{errorIndicatorColor}{#1}} +\newcommand{\infoDecorate}[1]{\coloredwave{infoIndicatorColor}{#1}} +\newcommand{\warningDecorate}[1]{\coloredwave{warningIndicatorColor}{#1}} \DefineVerbatimEnvironment{LeanVerbatim}{Verbatim} {commandchars=\\\{\},fontsize=\small,breaklines=true} \DefineVerbatimEnvironment{FileVerbatim}{Verbatim}{commandchars=\\\{\},fontsize=\small,breaklines=true,frame=single,framesep=2mm,numbers=left} @@ -124,6 +123,70 @@ \renewcommand{\cftsectionfont}{\normalfont\sffamily} \renewcommand{\cftchapterpagefont}{\normalfont\sffamily} \renewcommand{\cftsectionpagefont}{\normalfont\sffamily} +\providecommand{\versoKeyword}[1]{\textbf{#1}} +\providecommand{\versoConst}[1]{#1} +\providecommand{\versoVar}[1]{\textit{#1}} +\providecommand{\versoLiteral}[1]{#1} +\providecommand{\versoLiteralString}[1]{#1} +\providecommand{\versoDocComment}[1]{\textit{#1}} +\providecommand{\versoSort}[1]{#1} +\providecommand{\versoLevelVar}[1]{\textit{#1}} +\providecommand{\versoLevelConst}[1]{#1} +\providecommand{\versoLevelOp}[1]{#1} +\providecommand{\versoModuleName}[1]{#1} +\providecommand{\versoDelim}[1]{#1} +\providecommand{\versoOperator}[1]{#1} +\providecommand{\versoBracket}[1]{#1} +\providecommand{\versoSeparator}[1]{#1} +\providecommand{\versoLiteralNumber}[1]{#1} +\providecommand{\versoLiteralChar}[1]{#1} +\providecommand{\versoComment}[1]{#1} +\providecommand{\versoCommentDelim}[1]{#1} +\definecolor{versoCodeColor}{HTML}{000000} +\definecolor{versoConstColor}{HTML}{000000} +\definecolor{versoKeywordColor}{HTML}{000000} +\definecolor{versoVarColor}{HTML}{000000} +\definecolor{versoLiteralColor}{HTML}{000000} +\definecolor{versoLiteralStringColor}{HTML}{000000} +\definecolor{versoLiteralNumberColor}{HTML}{000000} +\definecolor{versoLiteralCharColor}{HTML}{000000} +\definecolor{versoDocCommentColor}{HTML}{000000} +\definecolor{versoCommentColor}{HTML}{000000} +\definecolor{versoCommentDelimColor}{HTML}{000000} +\definecolor{versoSortColor}{HTML}{000000} +\definecolor{versoLevelVarColor}{HTML}{000000} +\definecolor{versoLevelConstColor}{HTML}{000000} +\definecolor{versoLevelOpColor}{HTML}{000000} +\definecolor{versoModuleNameColor}{HTML}{000000} +\definecolor{versoDelimColor}{HTML}{000000} +\definecolor{versoOperatorColor}{HTML}{000000} +\definecolor{versoBracketColor}{HTML}{000000} +\definecolor{versoSeparatorColor}{HTML}{000000} +\definecolor{errorColor}{HTML}{CC0000} +\definecolor{warningColor}{HTML}{000000} +\definecolor{infoColor}{HTML}{000000} +\definecolor{errorIndicatorColor}{HTML}{FF0000} +\definecolor{warningIndicatorColor}{HTML}{D97706} +\definecolor{infoIndicatorColor}{HTML}{4777FF} +\renewcommand{\versoKeyword}[1]{\textcolor{versoKeywordColor}{\fontseries{eb}\fontshape{n}\selectfont #1}} +\renewcommand{\versoConst}[1]{\textcolor{versoConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoVar}[1]{\textcolor{versoVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLiteral}[1]{\textcolor{versoLiteralColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralString}[1]{\textcolor{versoLiteralStringColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralNumber}[1]{\textcolor{versoLiteralNumberColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralChar}[1]{\textcolor{versoLiteralCharColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDocComment}[1]{\textcolor{versoDocCommentColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoComment}[1]{\textcolor{versoCommentColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoCommentDelim}[1]{\textcolor{versoCommentDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSort}[1]{\textcolor{versoSortColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelVar}[1]{\textcolor{versoLevelVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLevelConst}[1]{\textcolor{versoLevelConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelOp}[1]{\textcolor{versoLevelOpColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoModuleName}[1]{\textcolor{versoModuleNameColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDelim}[1]{\textcolor{versoDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoOperator}[1]{\textcolor{versoOperatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoBracket}[1]{\textcolor{versoBracketColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSeparator}[1]{\textcolor{versoSeparatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} \setmonofont{DejaVu Sans Mono} \title{\sffamily Title of the Doc} @@ -144,72 +207,72 @@ \cleardoublepage Here is some code with vertical bars: \begin{LeanVerbatim} -\textbf{def} or := (\textit{·} \symbol{124}\symbol{124} \textit{·}) - +\versoKeyword{def} \versoConst{or} \versoDelim{:=} \versoBracket{(}\versoVar{·} \versoOperator{\symbol{124}\symbol{124}} \versoVar{·}\versoBracket{)} +\versoLiteral{} \end{LeanVerbatim} Here is some with a variety of interesting Unicode, including characters where UTF-16 is funky: \begin{LeanVerbatim} -\textbf{def} Set (\textit{α} : Type u) : Type u := \textit{α} → Prop - -\textbf{instance} : EmptyCollection (Set \textit{α}) \textbf{where} - emptyCollection := \textbf{fun} _ => False - -\textbf{instance} : Union (Set \textit{α}) \textbf{where} - union \textit{a} \textit{b} := \textbf{fun} \textit{x} => \textit{a} \textit{x} ∨ \textit{b} \textit{x} - -\textbf{instance} : Inter (Set \textit{α}) \textbf{where} - inter \textit{a} \textit{b} := \textbf{fun} \textit{x} => \textit{a} \textit{x} ∧ \textit{b} \textit{x} - -\textbf{instance} : Membership \textit{α} (Set \textit{α}) \textbf{where} - mem \textit{a} \textit{x} := \textit{a} \textit{x} - -@[\textbf{ext}] -\textbf{theorem} Set.ext \symbol{123}\textit{a} \textit{b} : Set \textit{α}\symbol{125} : - (∀ \textit{x}, \textit{x} ∈ \textit{a} ↔ \textit{x} ∈ \textit{b}) → \textit{a} = \textit{b} := \textbf{by} - \textbf{intro} \textit{h} - \textbf{funext} \textit{x} - \textbf{exact} propext (\textit{h} \textit{x}) - -\textbf{instance} : HasSubset (Set \textit{α}) \textbf{where} - Subset \textit{a} \textit{b} := ∀ \textit{x}, \textit{x} ∈ \textit{a} → \textit{x} ∈ \textit{b} - -@[\textbf{simp}, \textbf{grind} .] -\textbf{theorem} Set.subset_refl \symbol{123}\textit{a} : Set \textit{α}\symbol{125} : \textit{a} ⊆ \textit{a} := \textbf{by} - \textbf{simp} [(· ⊆ ·)] - -@[\textbf{grind} ←] -\textbf{theorem} Set.subset_union \symbol{123}\textit{a} \textit{b} \textit{c} : Set \textit{α}\symbol{125} : - \textit{a} ⊆ \textit{b} → \textit{a} ⊆ \textit{b} ∪ \textit{c} := \textbf{by} - \textbf{simp} [(· ⊆ ·), (· ∪ ·), (· ∈ ·)] - \textbf{intro} \textit{h} - \textbf{solve_by_elim} - -\textbf{def} Set.powerset (\textit{a} : Set \textit{α}) : Set (Set \textit{α}) := - \textbf{fun} (\textit{x} : Set \textit{α}) => \textit{x} ⊆ \textit{a} - -\textbf{notation} "𝒫 " \textit{x} => Set.powerset \textit{x} - -\textbf{theorem} Set.powerset_empty_nonempty : - ∃ (\textit{a} : Set \textit{α}), \textit{a} ∈ 𝒫 \symbol{123}\symbol{125} := \textbf{by} - \textbf{constructor} - \textbf{case} w => \textbf{exact} \symbol{123}\symbol{125} - \textbf{simp} [(· ∈ ·), powerset] - -@[\infoDecorate{\textbf{grind?} →}] -\textbf{theorem} Set.powerset_empty_unique (\textit{x} \textit{y} : Set \textit{α}) : - \textit{x} ∈ (𝒫 \symbol{123}\symbol{125}) → \textit{y} ∈ (𝒫 \symbol{123}\symbol{125}) → \textit{x} = \textit{y} := \textbf{by} - \textbf{intro} \textit{hx} \textit{hy} - \textbf{ext} \textit{x'} - \textbf{exact} (iff_false_right (\textit{hy} \textit{x'})).mpr (\textit{hx} \textit{x'}) - +\versoKeyword{def} \versoConst{Set} \versoBracket{(}\versoVar{α} \versoDelim{:} \versoSort{Type} \versoLevelVar{u}\versoBracket{)} \versoDelim{:} \versoSort{Type} \versoLevelVar{u} \versoDelim{:=} \versoVar{α} \versoOperator{→} \versoSort{Prop} + +\versoKeyword{instance} \versoDelim{:} \versoConst{EmptyCollection} \versoBracket{(}\versoConst{Set} \versoVar{α}\versoBracket{)} \versoKeyword{where} + \versoConst{emptyCollection} \versoDelim{:=} \versoKeyword{fun} \versoLiteral{_} \versoDelim{=>} \versoConst{False} + +\versoKeyword{instance} \versoDelim{:} \versoConst{Union} \versoBracket{(}\versoConst{Set} \versoVar{α}\versoBracket{)} \versoKeyword{where} + \versoConst{union} \versoVar{a} \versoVar{b} \versoDelim{:=} \versoKeyword{fun} \versoVar{x} \versoDelim{=>} \versoVar{a} \versoVar{x} \versoOperator{∨} \versoVar{b} \versoVar{x} + +\versoKeyword{instance} \versoDelim{:} \versoConst{Inter} \versoBracket{(}\versoConst{Set} \versoVar{α}\versoBracket{)} \versoKeyword{where} + \versoConst{inter} \versoVar{a} \versoVar{b} \versoDelim{:=} \versoKeyword{fun} \versoVar{x} \versoDelim{=>} \versoVar{a} \versoVar{x} \versoOperator{∧} \versoVar{b} \versoVar{x} + +\versoKeyword{instance} \versoDelim{:} \versoConst{Membership} \versoVar{α} \versoBracket{(}\versoConst{Set} \versoVar{α}\versoBracket{)} \versoKeyword{where} + \versoConst{mem} \versoVar{a} \versoVar{x} \versoDelim{:=} \versoVar{a} \versoVar{x} + +\versoLiteral{@[}\versoKeyword{ext}\versoBracket{]} +\versoKeyword{theorem} \versoConst{Set.ext} \versoBracket{\symbol{123}}\versoVar{a} \versoVar{b} \versoDelim{:} \versoConst{Set} \versoVar{α}\versoBracket{\symbol{125}} \versoDelim{:} + \versoBracket{(}\versoLiteral{∀} \versoVar{x}\versoSeparator{,} \versoVar{x} \versoOperator{∈} \versoVar{a} \versoOperator{↔} \versoVar{x} \versoOperator{∈} \versoVar{b}\versoBracket{)} \versoOperator{→} \versoVar{a} \versoOperator{=} \versoVar{b} \versoDelim{:=} \versoKeyword{by} + \versoKeyword{intro} \versoVar{h} + \versoKeyword{funext} \versoVar{x} + \versoKeyword{exact} \versoConst{propext} \versoBracket{(}\versoVar{h} \versoVar{x}\versoBracket{)} + +\versoKeyword{instance} \versoDelim{:} \versoConst{HasSubset} \versoBracket{(}\versoConst{Set} \versoVar{α}\versoBracket{)} \versoKeyword{where} + \versoConst{Subset} \versoVar{a} \versoVar{b} \versoDelim{:=} \versoLiteral{∀} \versoVar{x}\versoSeparator{,} \versoVar{x} \versoOperator{∈} \versoVar{a} \versoOperator{→} \versoVar{x} \versoOperator{∈} \versoVar{b} + +\versoLiteral{@[}\versoKeyword{simp}\versoSeparator{,} \versoKeyword{grind} \versoDelim{.}\versoBracket{]} +\versoKeyword{theorem} \versoConst{Set.subset_refl} \versoBracket{\symbol{123}}\versoVar{a} \versoDelim{:} \versoConst{Set} \versoVar{α}\versoBracket{\symbol{125}} \versoDelim{:} \versoVar{a} \versoOperator{⊆} \versoVar{a} \versoDelim{:=} \versoKeyword{by} + \versoKeyword{simp} \versoBracket{[}\versoBracket{(}\versoDelim{·} \versoOperator{⊆} \versoDelim{·}\versoBracket{)}\versoBracket{]} + +\versoLiteral{@[}\versoKeyword{grind} \versoDelim{←}\versoBracket{]} +\versoKeyword{theorem} \versoConst{Set.subset_union} \versoBracket{\symbol{123}}\versoVar{a} \versoVar{b} \versoVar{c} \versoDelim{:} \versoConst{Set} \versoVar{α}\versoBracket{\symbol{125}} \versoDelim{:} + \versoVar{a} \versoOperator{⊆} \versoVar{b} \versoOperator{→} \versoVar{a} \versoOperator{⊆} \versoVar{b} \versoOperator{∪} \versoVar{c} \versoDelim{:=} \versoKeyword{by} + \versoKeyword{simp} \versoBracket{[}\versoBracket{(}\versoDelim{·} \versoOperator{⊆} \versoDelim{·}\versoBracket{)}\versoSeparator{,} \versoBracket{(}\versoDelim{·} \versoOperator{∪} \versoDelim{·}\versoBracket{)}\versoSeparator{,} \versoBracket{(}\versoDelim{·} \versoOperator{∈} \versoDelim{·}\versoBracket{)}\versoBracket{]} + \versoKeyword{intro} \versoVar{h} + \versoKeyword{solve_by_elim} + +\versoKeyword{def} \versoConst{Set.powerset} \versoBracket{(}\versoVar{a} \versoDelim{:} \versoConst{Set} \versoVar{α}\versoBracket{)} \versoDelim{:} \versoConst{Set} \versoBracket{(}\versoConst{Set} \versoVar{α}\versoBracket{)} \versoDelim{:=} + \versoKeyword{fun} \versoBracket{(}\versoVar{x} \versoDelim{:} \versoConst{Set} \versoVar{α}\versoBracket{)} \versoDelim{=>} \versoVar{x} \versoOperator{⊆} \versoVar{a} + +\versoKeyword{notation} \versoLiteralString{"𝒫 "} \versoVar{x} \versoDelim{=>} \versoConst{Set.powerset} \versoVar{x} + +\versoKeyword{theorem} \versoConst{Set.powerset_empty_nonempty} \versoDelim{:} + \versoLiteral{∃} \versoBracket{(}\versoVar{a} \versoDelim{:} \versoConst{Set} \versoVar{α}\versoBracket{)}\versoSeparator{,} \versoVar{a} \versoOperator{∈} \versoLiteral{𝒫} \versoBracket{\symbol{123}}\versoBracket{\symbol{125}} \versoDelim{:=} \versoKeyword{by} + \versoKeyword{constructor} + \versoKeyword{case} \versoLiteral{w} \versoDelim{=>} \versoKeyword{exact} \versoBracket{\symbol{123}}\versoBracket{\symbol{125}} + \versoKeyword{simp} \versoBracket{[}\versoBracket{(}\versoDelim{·} \versoOperator{∈} \versoDelim{·}\versoBracket{)}\versoSeparator{,} \versoConst{powerset}\versoBracket{]} + +\versoLiteral{@[}\infoDecorate{\versoKeyword{grind?} \versoOperator{→}}\versoBracket{]} +\versoKeyword{theorem} \versoConst{Set.powerset_empty_unique} \versoBracket{(}\versoVar{x} \versoVar{y} \versoDelim{:} \versoConst{Set} \versoVar{α}\versoBracket{)} \versoDelim{:} + \versoVar{x} \versoOperator{∈} \versoBracket{(}\versoLiteral{𝒫} \versoBracket{\symbol{123}}\versoBracket{\symbol{125}}\versoBracket{)} \versoOperator{→} \versoVar{y} \versoOperator{∈} \versoBracket{(}\versoLiteral{𝒫} \versoBracket{\symbol{123}}\versoBracket{\symbol{125}}\versoBracket{)} \versoOperator{→} \versoVar{x} \versoOperator{=} \versoVar{y} \versoDelim{:=} \versoKeyword{by} + \versoKeyword{intro} \versoVar{hx} \versoVar{hy} + \versoKeyword{ext} \versoVar{x'} + \versoKeyword{exact} \versoBracket{(}\versoConst{iff_false_right} \versoBracket{(}\versoVar{hy} \versoVar{x'}\versoBracket{)}\versoBracket{)}\versoDelim{.}\versoConst{mpr} \versoBracket{(}\versoVar{hx} \versoVar{x'}\versoBracket{)} +\versoLiteral{} \end{LeanVerbatim} And now some inline code: \begin{itemize} -\item \LeanVerb|∀\textit{x} \textit{y} : Set _, \textit{x} ∈ ((𝒫 \textit{x}) ∪ (𝒫 \textit{y}))| -\item \LeanVerb|true \symbol{124}\symbol{124} false| -\item \LeanVerb|False → True| +\item \LeanVerb|\versoLiteral{∀}\versoVar{x} \versoVar{y} \versoDelim{:} \versoConst{Set} \versoLiteral{_}\versoSeparator{,} \versoVar{x} \versoOperator{∈} \versoBracket{(}\versoBracket{(}\versoLiteral{𝒫} \versoVar{x}\versoBracket{)} \versoOperator{∪} \versoBracket{(}\versoLiteral{𝒫} \versoVar{y}\versoBracket{)}\versoBracket{)}| +\item \LeanVerb|\versoConst{true} \versoOperator{\symbol{124}\symbol{124}} \versoConst{false}| +\item \LeanVerb|\versoConst{False} \versoOperator{→} \versoConst{True}| \end{itemize} diff --git a/src/tests/integration/diagram-doc/expected/tex/main.tex b/src/tests/integration/diagram-doc/expected/tex/main.tex index 47d521914..5b8dcf60e 100644 --- a/src/tests/integration/diagram-doc/expected/tex/main.tex +++ b/src/tests/integration/diagram-doc/expected/tex/main.tex @@ -51,12 +51,11 @@ % Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro \newunicodechar{‑}{-} -\definecolor{errorColor}{HTML}{B91C1C} -\definecolor{infoColor}{HTML}{1E6BB8} -\definecolor{warningColor}{HTML}{D97706} -\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}} -\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}} -\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}} +% Decoration accents (wavy underlines) use the *indicator* colors, distinct from the message +% text colors. The theme block below redefines both. +\newcommand{\errorDecorate}[1]{\coloredwave{errorIndicatorColor}{#1}} +\newcommand{\infoDecorate}[1]{\coloredwave{infoIndicatorColor}{#1}} +\newcommand{\warningDecorate}[1]{\coloredwave{warningIndicatorColor}{#1}} \DefineVerbatimEnvironment{LeanVerbatim}{Verbatim} {commandchars=\\\{\},fontsize=\small,breaklines=true} \DefineVerbatimEnvironment{FileVerbatim}{Verbatim}{commandchars=\\\{\},fontsize=\small,breaklines=true,frame=single,framesep=2mm,numbers=left} @@ -124,6 +123,70 @@ \renewcommand{\cftsectionfont}{\normalfont\sffamily} \renewcommand{\cftchapterpagefont}{\normalfont\sffamily} \renewcommand{\cftsectionpagefont}{\normalfont\sffamily} +\providecommand{\versoKeyword}[1]{\textbf{#1}} +\providecommand{\versoConst}[1]{#1} +\providecommand{\versoVar}[1]{\textit{#1}} +\providecommand{\versoLiteral}[1]{#1} +\providecommand{\versoLiteralString}[1]{#1} +\providecommand{\versoDocComment}[1]{\textit{#1}} +\providecommand{\versoSort}[1]{#1} +\providecommand{\versoLevelVar}[1]{\textit{#1}} +\providecommand{\versoLevelConst}[1]{#1} +\providecommand{\versoLevelOp}[1]{#1} +\providecommand{\versoModuleName}[1]{#1} +\providecommand{\versoDelim}[1]{#1} +\providecommand{\versoOperator}[1]{#1} +\providecommand{\versoBracket}[1]{#1} +\providecommand{\versoSeparator}[1]{#1} +\providecommand{\versoLiteralNumber}[1]{#1} +\providecommand{\versoLiteralChar}[1]{#1} +\providecommand{\versoComment}[1]{#1} +\providecommand{\versoCommentDelim}[1]{#1} +\definecolor{versoCodeColor}{HTML}{000000} +\definecolor{versoConstColor}{HTML}{000000} +\definecolor{versoKeywordColor}{HTML}{000000} +\definecolor{versoVarColor}{HTML}{000000} +\definecolor{versoLiteralColor}{HTML}{000000} +\definecolor{versoLiteralStringColor}{HTML}{000000} +\definecolor{versoLiteralNumberColor}{HTML}{000000} +\definecolor{versoLiteralCharColor}{HTML}{000000} +\definecolor{versoDocCommentColor}{HTML}{000000} +\definecolor{versoCommentColor}{HTML}{000000} +\definecolor{versoCommentDelimColor}{HTML}{000000} +\definecolor{versoSortColor}{HTML}{000000} +\definecolor{versoLevelVarColor}{HTML}{000000} +\definecolor{versoLevelConstColor}{HTML}{000000} +\definecolor{versoLevelOpColor}{HTML}{000000} +\definecolor{versoModuleNameColor}{HTML}{000000} +\definecolor{versoDelimColor}{HTML}{000000} +\definecolor{versoOperatorColor}{HTML}{000000} +\definecolor{versoBracketColor}{HTML}{000000} +\definecolor{versoSeparatorColor}{HTML}{000000} +\definecolor{errorColor}{HTML}{CC0000} +\definecolor{warningColor}{HTML}{000000} +\definecolor{infoColor}{HTML}{000000} +\definecolor{errorIndicatorColor}{HTML}{FF0000} +\definecolor{warningIndicatorColor}{HTML}{D97706} +\definecolor{infoIndicatorColor}{HTML}{4777FF} +\renewcommand{\versoKeyword}[1]{\textcolor{versoKeywordColor}{\fontseries{eb}\fontshape{n}\selectfont #1}} +\renewcommand{\versoConst}[1]{\textcolor{versoConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoVar}[1]{\textcolor{versoVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLiteral}[1]{\textcolor{versoLiteralColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralString}[1]{\textcolor{versoLiteralStringColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralNumber}[1]{\textcolor{versoLiteralNumberColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralChar}[1]{\textcolor{versoLiteralCharColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDocComment}[1]{\textcolor{versoDocCommentColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoComment}[1]{\textcolor{versoCommentColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoCommentDelim}[1]{\textcolor{versoCommentDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSort}[1]{\textcolor{versoSortColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelVar}[1]{\textcolor{versoLevelVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLevelConst}[1]{\textcolor{versoLevelConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelOp}[1]{\textcolor{versoLevelOpColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoModuleName}[1]{\textcolor{versoModuleNameColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDelim}[1]{\textcolor{versoDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoOperator}[1]{\textcolor{versoOperatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoBracket}[1]{\textcolor{versoBracketColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSeparator}[1]{\textcolor{versoSeparatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} \setmonofont{DejaVu Sans Mono} \title{\sffamily Diagrams in the Manual genre} diff --git a/src/tests/integration/extra-files-doc/expected/tex/main.tex b/src/tests/integration/extra-files-doc/expected/tex/main.tex index c9aa89ea8..b6dfe70c2 100644 --- a/src/tests/integration/extra-files-doc/expected/tex/main.tex +++ b/src/tests/integration/extra-files-doc/expected/tex/main.tex @@ -51,12 +51,11 @@ % Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro \newunicodechar{‑}{-} -\definecolor{errorColor}{HTML}{B91C1C} -\definecolor{infoColor}{HTML}{1E6BB8} -\definecolor{warningColor}{HTML}{D97706} -\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}} -\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}} -\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}} +% Decoration accents (wavy underlines) use the *indicator* colors, distinct from the message +% text colors. The theme block below redefines both. +\newcommand{\errorDecorate}[1]{\coloredwave{errorIndicatorColor}{#1}} +\newcommand{\infoDecorate}[1]{\coloredwave{infoIndicatorColor}{#1}} +\newcommand{\warningDecorate}[1]{\coloredwave{warningIndicatorColor}{#1}} \DefineVerbatimEnvironment{LeanVerbatim}{Verbatim} {commandchars=\\\{\},fontsize=\small,breaklines=true} \DefineVerbatimEnvironment{FileVerbatim}{Verbatim}{commandchars=\\\{\},fontsize=\small,breaklines=true,frame=single,framesep=2mm,numbers=left} @@ -124,6 +123,70 @@ \renewcommand{\cftsectionfont}{\normalfont\sffamily} \renewcommand{\cftchapterpagefont}{\normalfont\sffamily} \renewcommand{\cftsectionpagefont}{\normalfont\sffamily} +\providecommand{\versoKeyword}[1]{\textbf{#1}} +\providecommand{\versoConst}[1]{#1} +\providecommand{\versoVar}[1]{\textit{#1}} +\providecommand{\versoLiteral}[1]{#1} +\providecommand{\versoLiteralString}[1]{#1} +\providecommand{\versoDocComment}[1]{\textit{#1}} +\providecommand{\versoSort}[1]{#1} +\providecommand{\versoLevelVar}[1]{\textit{#1}} +\providecommand{\versoLevelConst}[1]{#1} +\providecommand{\versoLevelOp}[1]{#1} +\providecommand{\versoModuleName}[1]{#1} +\providecommand{\versoDelim}[1]{#1} +\providecommand{\versoOperator}[1]{#1} +\providecommand{\versoBracket}[1]{#1} +\providecommand{\versoSeparator}[1]{#1} +\providecommand{\versoLiteralNumber}[1]{#1} +\providecommand{\versoLiteralChar}[1]{#1} +\providecommand{\versoComment}[1]{#1} +\providecommand{\versoCommentDelim}[1]{#1} +\definecolor{versoCodeColor}{HTML}{000000} +\definecolor{versoConstColor}{HTML}{000000} +\definecolor{versoKeywordColor}{HTML}{000000} +\definecolor{versoVarColor}{HTML}{000000} +\definecolor{versoLiteralColor}{HTML}{000000} +\definecolor{versoLiteralStringColor}{HTML}{000000} +\definecolor{versoLiteralNumberColor}{HTML}{000000} +\definecolor{versoLiteralCharColor}{HTML}{000000} +\definecolor{versoDocCommentColor}{HTML}{000000} +\definecolor{versoCommentColor}{HTML}{000000} +\definecolor{versoCommentDelimColor}{HTML}{000000} +\definecolor{versoSortColor}{HTML}{000000} +\definecolor{versoLevelVarColor}{HTML}{000000} +\definecolor{versoLevelConstColor}{HTML}{000000} +\definecolor{versoLevelOpColor}{HTML}{000000} +\definecolor{versoModuleNameColor}{HTML}{000000} +\definecolor{versoDelimColor}{HTML}{000000} +\definecolor{versoOperatorColor}{HTML}{000000} +\definecolor{versoBracketColor}{HTML}{000000} +\definecolor{versoSeparatorColor}{HTML}{000000} +\definecolor{errorColor}{HTML}{CC0000} +\definecolor{warningColor}{HTML}{000000} +\definecolor{infoColor}{HTML}{000000} +\definecolor{errorIndicatorColor}{HTML}{FF0000} +\definecolor{warningIndicatorColor}{HTML}{D97706} +\definecolor{infoIndicatorColor}{HTML}{4777FF} +\renewcommand{\versoKeyword}[1]{\textcolor{versoKeywordColor}{\fontseries{eb}\fontshape{n}\selectfont #1}} +\renewcommand{\versoConst}[1]{\textcolor{versoConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoVar}[1]{\textcolor{versoVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLiteral}[1]{\textcolor{versoLiteralColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralString}[1]{\textcolor{versoLiteralStringColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralNumber}[1]{\textcolor{versoLiteralNumberColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralChar}[1]{\textcolor{versoLiteralCharColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDocComment}[1]{\textcolor{versoDocCommentColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoComment}[1]{\textcolor{versoCommentColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoCommentDelim}[1]{\textcolor{versoCommentDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSort}[1]{\textcolor{versoSortColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelVar}[1]{\textcolor{versoLevelVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLevelConst}[1]{\textcolor{versoLevelConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelOp}[1]{\textcolor{versoLevelOpColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoModuleName}[1]{\textcolor{versoModuleNameColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDelim}[1]{\textcolor{versoDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoOperator}[1]{\textcolor{versoOperatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoBracket}[1]{\textcolor{versoBracketColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSeparator}[1]{\textcolor{versoSeparatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} \setmonofont{DejaVu Sans Mono} \title{\sffamily Extra Files Test Document} diff --git a/src/tests/integration/front-matter-doc/expected/tex/main.tex b/src/tests/integration/front-matter-doc/expected/tex/main.tex index 371a84f8e..037e23e12 100644 --- a/src/tests/integration/front-matter-doc/expected/tex/main.tex +++ b/src/tests/integration/front-matter-doc/expected/tex/main.tex @@ -51,12 +51,11 @@ % Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro \newunicodechar{‑}{-} -\definecolor{errorColor}{HTML}{B91C1C} -\definecolor{infoColor}{HTML}{1E6BB8} -\definecolor{warningColor}{HTML}{D97706} -\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}} -\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}} -\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}} +% Decoration accents (wavy underlines) use the *indicator* colors, distinct from the message +% text colors. The theme block below redefines both. +\newcommand{\errorDecorate}[1]{\coloredwave{errorIndicatorColor}{#1}} +\newcommand{\infoDecorate}[1]{\coloredwave{infoIndicatorColor}{#1}} +\newcommand{\warningDecorate}[1]{\coloredwave{warningIndicatorColor}{#1}} \DefineVerbatimEnvironment{LeanVerbatim}{Verbatim} {commandchars=\\\{\},fontsize=\small,breaklines=true} \DefineVerbatimEnvironment{FileVerbatim}{Verbatim}{commandchars=\\\{\},fontsize=\small,breaklines=true,frame=single,framesep=2mm,numbers=left} @@ -124,6 +123,70 @@ \renewcommand{\cftsectionfont}{\normalfont\sffamily} \renewcommand{\cftchapterpagefont}{\normalfont\sffamily} \renewcommand{\cftsectionpagefont}{\normalfont\sffamily} +\providecommand{\versoKeyword}[1]{\textbf{#1}} +\providecommand{\versoConst}[1]{#1} +\providecommand{\versoVar}[1]{\textit{#1}} +\providecommand{\versoLiteral}[1]{#1} +\providecommand{\versoLiteralString}[1]{#1} +\providecommand{\versoDocComment}[1]{\textit{#1}} +\providecommand{\versoSort}[1]{#1} +\providecommand{\versoLevelVar}[1]{\textit{#1}} +\providecommand{\versoLevelConst}[1]{#1} +\providecommand{\versoLevelOp}[1]{#1} +\providecommand{\versoModuleName}[1]{#1} +\providecommand{\versoDelim}[1]{#1} +\providecommand{\versoOperator}[1]{#1} +\providecommand{\versoBracket}[1]{#1} +\providecommand{\versoSeparator}[1]{#1} +\providecommand{\versoLiteralNumber}[1]{#1} +\providecommand{\versoLiteralChar}[1]{#1} +\providecommand{\versoComment}[1]{#1} +\providecommand{\versoCommentDelim}[1]{#1} +\definecolor{versoCodeColor}{HTML}{000000} +\definecolor{versoConstColor}{HTML}{000000} +\definecolor{versoKeywordColor}{HTML}{000000} +\definecolor{versoVarColor}{HTML}{000000} +\definecolor{versoLiteralColor}{HTML}{000000} +\definecolor{versoLiteralStringColor}{HTML}{000000} +\definecolor{versoLiteralNumberColor}{HTML}{000000} +\definecolor{versoLiteralCharColor}{HTML}{000000} +\definecolor{versoDocCommentColor}{HTML}{000000} +\definecolor{versoCommentColor}{HTML}{000000} +\definecolor{versoCommentDelimColor}{HTML}{000000} +\definecolor{versoSortColor}{HTML}{000000} +\definecolor{versoLevelVarColor}{HTML}{000000} +\definecolor{versoLevelConstColor}{HTML}{000000} +\definecolor{versoLevelOpColor}{HTML}{000000} +\definecolor{versoModuleNameColor}{HTML}{000000} +\definecolor{versoDelimColor}{HTML}{000000} +\definecolor{versoOperatorColor}{HTML}{000000} +\definecolor{versoBracketColor}{HTML}{000000} +\definecolor{versoSeparatorColor}{HTML}{000000} +\definecolor{errorColor}{HTML}{CC0000} +\definecolor{warningColor}{HTML}{000000} +\definecolor{infoColor}{HTML}{000000} +\definecolor{errorIndicatorColor}{HTML}{FF0000} +\definecolor{warningIndicatorColor}{HTML}{D97706} +\definecolor{infoIndicatorColor}{HTML}{4777FF} +\renewcommand{\versoKeyword}[1]{\textcolor{versoKeywordColor}{\fontseries{eb}\fontshape{n}\selectfont #1}} +\renewcommand{\versoConst}[1]{\textcolor{versoConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoVar}[1]{\textcolor{versoVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLiteral}[1]{\textcolor{versoLiteralColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralString}[1]{\textcolor{versoLiteralStringColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralNumber}[1]{\textcolor{versoLiteralNumberColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralChar}[1]{\textcolor{versoLiteralCharColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDocComment}[1]{\textcolor{versoDocCommentColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoComment}[1]{\textcolor{versoCommentColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoCommentDelim}[1]{\textcolor{versoCommentDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSort}[1]{\textcolor{versoSortColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelVar}[1]{\textcolor{versoLevelVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLevelConst}[1]{\textcolor{versoLevelConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelOp}[1]{\textcolor{versoLevelOpColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoModuleName}[1]{\textcolor{versoModuleNameColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDelim}[1]{\textcolor{versoDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoOperator}[1]{\textcolor{versoOperatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoBracket}[1]{\textcolor{versoBracketColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSeparator}[1]{\textcolor{versoSeparatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} \setmonofont{DejaVu Sans Mono} \title{\sffamily Front Matter Test Document} diff --git a/src/tests/integration/inheritance-doc/expected/tex/main.tex b/src/tests/integration/inheritance-doc/expected/tex/main.tex index 0600aab1b..b2170fbbf 100644 --- a/src/tests/integration/inheritance-doc/expected/tex/main.tex +++ b/src/tests/integration/inheritance-doc/expected/tex/main.tex @@ -51,12 +51,11 @@ % Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro \newunicodechar{‑}{-} -\definecolor{errorColor}{HTML}{B91C1C} -\definecolor{infoColor}{HTML}{1E6BB8} -\definecolor{warningColor}{HTML}{D97706} -\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}} -\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}} -\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}} +% Decoration accents (wavy underlines) use the *indicator* colors, distinct from the message +% text colors. The theme block below redefines both. +\newcommand{\errorDecorate}[1]{\coloredwave{errorIndicatorColor}{#1}} +\newcommand{\infoDecorate}[1]{\coloredwave{infoIndicatorColor}{#1}} +\newcommand{\warningDecorate}[1]{\coloredwave{warningIndicatorColor}{#1}} \DefineVerbatimEnvironment{LeanVerbatim}{Verbatim} {commandchars=\\\{\},fontsize=\small,breaklines=true} \DefineVerbatimEnvironment{FileVerbatim}{Verbatim}{commandchars=\\\{\},fontsize=\small,breaklines=true,frame=single,framesep=2mm,numbers=left} @@ -124,6 +123,70 @@ \renewcommand{\cftsectionfont}{\normalfont\sffamily} \renewcommand{\cftchapterpagefont}{\normalfont\sffamily} \renewcommand{\cftsectionpagefont}{\normalfont\sffamily} +\providecommand{\versoKeyword}[1]{\textbf{#1}} +\providecommand{\versoConst}[1]{#1} +\providecommand{\versoVar}[1]{\textit{#1}} +\providecommand{\versoLiteral}[1]{#1} +\providecommand{\versoLiteralString}[1]{#1} +\providecommand{\versoDocComment}[1]{\textit{#1}} +\providecommand{\versoSort}[1]{#1} +\providecommand{\versoLevelVar}[1]{\textit{#1}} +\providecommand{\versoLevelConst}[1]{#1} +\providecommand{\versoLevelOp}[1]{#1} +\providecommand{\versoModuleName}[1]{#1} +\providecommand{\versoDelim}[1]{#1} +\providecommand{\versoOperator}[1]{#1} +\providecommand{\versoBracket}[1]{#1} +\providecommand{\versoSeparator}[1]{#1} +\providecommand{\versoLiteralNumber}[1]{#1} +\providecommand{\versoLiteralChar}[1]{#1} +\providecommand{\versoComment}[1]{#1} +\providecommand{\versoCommentDelim}[1]{#1} +\definecolor{versoCodeColor}{HTML}{000000} +\definecolor{versoConstColor}{HTML}{000000} +\definecolor{versoKeywordColor}{HTML}{000000} +\definecolor{versoVarColor}{HTML}{000000} +\definecolor{versoLiteralColor}{HTML}{000000} +\definecolor{versoLiteralStringColor}{HTML}{000000} +\definecolor{versoLiteralNumberColor}{HTML}{000000} +\definecolor{versoLiteralCharColor}{HTML}{000000} +\definecolor{versoDocCommentColor}{HTML}{000000} +\definecolor{versoCommentColor}{HTML}{000000} +\definecolor{versoCommentDelimColor}{HTML}{000000} +\definecolor{versoSortColor}{HTML}{000000} +\definecolor{versoLevelVarColor}{HTML}{000000} +\definecolor{versoLevelConstColor}{HTML}{000000} +\definecolor{versoLevelOpColor}{HTML}{000000} +\definecolor{versoModuleNameColor}{HTML}{000000} +\definecolor{versoDelimColor}{HTML}{000000} +\definecolor{versoOperatorColor}{HTML}{000000} +\definecolor{versoBracketColor}{HTML}{000000} +\definecolor{versoSeparatorColor}{HTML}{000000} +\definecolor{errorColor}{HTML}{CC0000} +\definecolor{warningColor}{HTML}{000000} +\definecolor{infoColor}{HTML}{000000} +\definecolor{errorIndicatorColor}{HTML}{FF0000} +\definecolor{warningIndicatorColor}{HTML}{D97706} +\definecolor{infoIndicatorColor}{HTML}{4777FF} +\renewcommand{\versoKeyword}[1]{\textcolor{versoKeywordColor}{\fontseries{eb}\fontshape{n}\selectfont #1}} +\renewcommand{\versoConst}[1]{\textcolor{versoConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoVar}[1]{\textcolor{versoVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLiteral}[1]{\textcolor{versoLiteralColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralString}[1]{\textcolor{versoLiteralStringColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralNumber}[1]{\textcolor{versoLiteralNumberColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralChar}[1]{\textcolor{versoLiteralCharColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDocComment}[1]{\textcolor{versoDocCommentColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoComment}[1]{\textcolor{versoCommentColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoCommentDelim}[1]{\textcolor{versoCommentDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSort}[1]{\textcolor{versoSortColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelVar}[1]{\textcolor{versoLevelVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLevelConst}[1]{\textcolor{versoLevelConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelOp}[1]{\textcolor{versoLevelOpColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoModuleName}[1]{\textcolor{versoModuleNameColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDelim}[1]{\textcolor{versoDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoOperator}[1]{\textcolor{versoOperatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoBracket}[1]{\textcolor{versoBracketColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSeparator}[1]{\textcolor{versoSeparatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} \setmonofont{DejaVu Sans Mono} \title{\sffamily Title of the Doc} @@ -143,7 +206,7 @@ \cleardoublepage \begin{docstringBox}{structure} -\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends : Type|\tcblower Documentation for FooExtends\par\noindent\textbf{Constructor}\par \par \LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends.\allowbreak{}mk|\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends\par\noindent\textbf{Fields}\par \par \LeanVerb|bar\-Field1| : \LeanVerb|Bool|\par Inherited from \LeanVerb|Bar\-Extended|\par \LeanVerb|bar\-Field2| : \LeanVerb|Unit|\par Inherited from \LeanVerb|Bar\-Extended|\par \LeanVerb|foo\-Field1| : \LeanVerb|Nat|\par Documentation for fooField1\par \LeanVerb|foo\-Field2| : \LeanVerb|String|\par Documentation for fooField2 +\LeanVerb|\versoConst{Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends} \versoLiteral{:} \versoSort{Type}|\tcblower Documentation for FooExtends\par\noindent\textbf{Constructor}\par \par \LeanVerb|\versoConst{Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends.\allowbreak{}mk}|\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends\par\noindent\textbf{Fields}\par \par \LeanVerb|\versoLiteral{bar\-Field1}| : \LeanVerb|\versoConst{Bool}|\par Inherited from \LeanVerb|\versoConst{Bar\-Extended}|\par \LeanVerb|\versoLiteral{bar\-Field2}| : \LeanVerb|\versoConst{Unit}|\par Inherited from \LeanVerb|\versoConst{Bar\-Extended}|\par \LeanVerb|\versoConst{foo\-Field1}| : \LeanVerb|\versoConst{Nat}|\par Documentation for fooField1\par \LeanVerb|\versoConst{foo\-Field2}| : \LeanVerb|\versoConst{String}|\par Documentation for fooField2 \end{docstringBox} diff --git a/src/tests/integration/sample-doc/expected/tex/main.tex b/src/tests/integration/sample-doc/expected/tex/main.tex index 7d0f48a24..47916a36d 100644 --- a/src/tests/integration/sample-doc/expected/tex/main.tex +++ b/src/tests/integration/sample-doc/expected/tex/main.tex @@ -51,12 +51,11 @@ % Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro \newunicodechar{‑}{-} -\definecolor{errorColor}{HTML}{B91C1C} -\definecolor{infoColor}{HTML}{1E6BB8} -\definecolor{warningColor}{HTML}{D97706} -\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}} -\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}} -\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}} +% Decoration accents (wavy underlines) use the *indicator* colors, distinct from the message +% text colors. The theme block below redefines both. +\newcommand{\errorDecorate}[1]{\coloredwave{errorIndicatorColor}{#1}} +\newcommand{\infoDecorate}[1]{\coloredwave{infoIndicatorColor}{#1}} +\newcommand{\warningDecorate}[1]{\coloredwave{warningIndicatorColor}{#1}} \DefineVerbatimEnvironment{LeanVerbatim}{Verbatim} {commandchars=\\\{\},fontsize=\small,breaklines=true} \DefineVerbatimEnvironment{FileVerbatim}{Verbatim}{commandchars=\\\{\},fontsize=\small,breaklines=true,frame=single,framesep=2mm,numbers=left} @@ -124,6 +123,70 @@ \renewcommand{\cftsectionfont}{\normalfont\sffamily} \renewcommand{\cftchapterpagefont}{\normalfont\sffamily} \renewcommand{\cftsectionpagefont}{\normalfont\sffamily} +\providecommand{\versoKeyword}[1]{\textbf{#1}} +\providecommand{\versoConst}[1]{#1} +\providecommand{\versoVar}[1]{\textit{#1}} +\providecommand{\versoLiteral}[1]{#1} +\providecommand{\versoLiteralString}[1]{#1} +\providecommand{\versoDocComment}[1]{\textit{#1}} +\providecommand{\versoSort}[1]{#1} +\providecommand{\versoLevelVar}[1]{\textit{#1}} +\providecommand{\versoLevelConst}[1]{#1} +\providecommand{\versoLevelOp}[1]{#1} +\providecommand{\versoModuleName}[1]{#1} +\providecommand{\versoDelim}[1]{#1} +\providecommand{\versoOperator}[1]{#1} +\providecommand{\versoBracket}[1]{#1} +\providecommand{\versoSeparator}[1]{#1} +\providecommand{\versoLiteralNumber}[1]{#1} +\providecommand{\versoLiteralChar}[1]{#1} +\providecommand{\versoComment}[1]{#1} +\providecommand{\versoCommentDelim}[1]{#1} +\definecolor{versoCodeColor}{HTML}{000000} +\definecolor{versoConstColor}{HTML}{000000} +\definecolor{versoKeywordColor}{HTML}{000000} +\definecolor{versoVarColor}{HTML}{000000} +\definecolor{versoLiteralColor}{HTML}{000000} +\definecolor{versoLiteralStringColor}{HTML}{000000} +\definecolor{versoLiteralNumberColor}{HTML}{000000} +\definecolor{versoLiteralCharColor}{HTML}{000000} +\definecolor{versoDocCommentColor}{HTML}{000000} +\definecolor{versoCommentColor}{HTML}{000000} +\definecolor{versoCommentDelimColor}{HTML}{000000} +\definecolor{versoSortColor}{HTML}{000000} +\definecolor{versoLevelVarColor}{HTML}{000000} +\definecolor{versoLevelConstColor}{HTML}{000000} +\definecolor{versoLevelOpColor}{HTML}{000000} +\definecolor{versoModuleNameColor}{HTML}{000000} +\definecolor{versoDelimColor}{HTML}{000000} +\definecolor{versoOperatorColor}{HTML}{000000} +\definecolor{versoBracketColor}{HTML}{000000} +\definecolor{versoSeparatorColor}{HTML}{000000} +\definecolor{errorColor}{HTML}{CC0000} +\definecolor{warningColor}{HTML}{000000} +\definecolor{infoColor}{HTML}{000000} +\definecolor{errorIndicatorColor}{HTML}{FF0000} +\definecolor{warningIndicatorColor}{HTML}{D97706} +\definecolor{infoIndicatorColor}{HTML}{4777FF} +\renewcommand{\versoKeyword}[1]{\textcolor{versoKeywordColor}{\fontseries{eb}\fontshape{n}\selectfont #1}} +\renewcommand{\versoConst}[1]{\textcolor{versoConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoVar}[1]{\textcolor{versoVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLiteral}[1]{\textcolor{versoLiteralColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralString}[1]{\textcolor{versoLiteralStringColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralNumber}[1]{\textcolor{versoLiteralNumberColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLiteralChar}[1]{\textcolor{versoLiteralCharColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDocComment}[1]{\textcolor{versoDocCommentColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoComment}[1]{\textcolor{versoCommentColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoCommentDelim}[1]{\textcolor{versoCommentDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSort}[1]{\textcolor{versoSortColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelVar}[1]{\textcolor{versoLevelVarColor}{\fontseries{m}\fontshape{it}\selectfont #1}} +\renewcommand{\versoLevelConst}[1]{\textcolor{versoLevelConstColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoLevelOp}[1]{\textcolor{versoLevelOpColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoModuleName}[1]{\textcolor{versoModuleNameColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoDelim}[1]{\textcolor{versoDelimColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoOperator}[1]{\textcolor{versoOperatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoBracket}[1]{\textcolor{versoBracketColor}{\fontseries{m}\fontshape{n}\selectfont #1}} +\renewcommand{\versoSeparator}[1]{\textcolor{versoSeparatorColor}{\fontseries{m}\fontshape{n}\selectfont #1}} \setmonofont{DejaVu Sans Mono} \title{\sffamily Title of the Doc} @@ -143,7 +206,7 @@ \cleardoublepage \begin{docstringBox}{def} -\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Sample\-Doc.\allowbreak{}sample_constant : Type|\tcblower This is a docstring.Here's some more text with a \LeanVerb|code inline| in it. +\LeanVerb|\versoConst{Verso.\allowbreak{}Integration.\allowbreak{}Sample\-Doc.\allowbreak{}sample_constant} \versoLiteral{:} \versoSort{Type}|\tcblower This is a docstring.Here's some more text with a \LeanVerb|code inline| in it. Here's when a \LeanVerb|code inline| occurs right before a line break.And then here's a paragraph break. \end{docstringBox} diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 7156ff13e..538854935 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -11,6 +11,12 @@ import Verso.Doc.Html import Verso.Output.TeX import Verso.Output.Html import Verso.Output.Html.CssVars +import Verso.Theme.Code +import Verso.Theme.Code.Defaults +import VersoManual.Theme +import VersoManual.Theme.Defaults +import VersoManual.Theme.Emit +import VersoManual.Theme.Assets import Verso.Output.Html.KaTeX import Verso.Output.Html.ElasticLunr import Verso.Doc.Lsp @@ -60,6 +66,7 @@ open Verso.Code (LinkTargets) open Verso.Code.Hover (Dedup State) open Verso.ArgParse open Verso (Logger Severity withLogger BuildLogT) +open Verso.Theme (ThemeRegistry) namespace Verso.Genre @@ -231,17 +238,74 @@ structure Config extends HtmlConfig, TeXConfig, OutputConfig where /-- Global priorities that control the relative ranking of the semantic (quick-jump) and full-text - search result streams, each on a scale from {lit}`0` to {lit}`99`. Defaults are {lit}`50` on + search result streams, each on a scale from `0` to `99`. Defaults are `50` on both sides. -/ searchPriorities : SearchPriorities := {} + + /-- + When true (the default), it is an error if no theme is accessible. When false the same problems + become warnings. + + A theme counts as "accessible" if its `ManualTheme.checkAccessibility` returns no + issues. In other words: + * Every checked color pair meets the WCAG AA contrast threshold + * Every pair of token colors stays mutually distinguishable under each of the three dichromacies + (`protanopia`, `deuteranopia`, `tritanopia`). + + With a single registered theme, that theme must be accessible. With multiple themes, there must be + at least one accessible light theme and one accessible dark theme so a reader on either appearance + can pick a usable theme. + -/ + strictThemeCoverage : Bool := true + + /-- + When `true` (the default), the build errors if the configured `defaultLightTheme` or + `defaultDarkTheme` has any accessibility issues. When false the same problems become build-log + warnings and the build proceeds. + -/ + strictDefaultThemeAccessibility : Bool := true + + /-- + When `true` (the default), every registered theme that has accessibility issues emits a build-log + warning that names the theme and the specific issues. Setting this to `false` silences these + per-theme warnings — useful when shipping a documented trade-off (for example the canonical + Solarized palette, whose token colors are below WCAG AA's 4.5:1 contrast threshold for normal text + by design). + -/ + warnPerThemeAccessibility : Bool := true deriving ToJson, FromJson +open Lean in +open Verso.Theme in structure RenderConfig extends Config where /-- How to insert links in rendered code -/ linkTargets : TraverseState → Multi.AllRemotes → LinkTargets Manual.TraverseContext := (·.localTargets ++ ·.remoteTargets) + /-- + The manual themes that should be available in the picker. When `none` (the default), every + theme registered with `@[manual_theme]` is available. + -/ + availableThemes : Option NameSet := none + /-- + The default light-appearance theme. Its registration name must be a registered + `ManualTheme` whose appearance is `.light`. + -/ + defaultLightTheme : Name := ``ManualTheme.ink + /-- + The default dark-appearance theme. Its registration name must be a registered + `ManualTheme` whose appearance is `.dark`. + -/ + defaultDarkTheme : Name := ``ManualTheme.argent + /-- + The appearance new readers start in. + -/ + defaultAppearance : ThemeMode := .followSystem + /-- + The {name}`CodeTheme` used for PDF output. + -/ + pdfCodeTheme : CodeTheme := CodeTheme.ink namespace Config @@ -313,14 +377,16 @@ def TraverseState.ofConfig (config : HtmlConfig) : TraverseState := Id.run do st := st.addLicenseInfo li return st -/-- -The monad in which manuals are converted to an output format. --/ -abbrev EmitM : Type → Type := ReaderT ExtensionImpls (BuildLogT IO) def traverse (text : Part Manual) (config : Config) : EmitM (Part Manual × TraverseState) := do let topCtxt : Manual.TraverseContext := { draft := config.draft } let mut state : Manual.TraverseState := .ofConfig config.toHtmlConfig + -- Themes contribute their own third-party licenses (color palettes, fonts) on top of the + -- HtmlFeature ones already collected by `TraverseState.ofConfig`. + let registry ← readThe ThemeRegistry + for (_, theme) in registry do + for li in theme.licenses do + state := state.addLicenseInfo li let mut text := text if !config.draft then text := removeDraftParts text @@ -372,8 +438,57 @@ where isUnnumbered (p : Part Manual) : Bool := p.metadata.map (·.number) |>.isEqSome false open IO.FS in -def emitTeX (config : Config) (text : Part Manual) : EmitM Unit := do - let (text, state) ← traverse text config +/-- +Writes every theme-related asset for an output root: the multi-theme `verso-themes.css`, the +picker `.js`/`.css`, the `window.versoThemes` data file, every theme's font bytes and bundled +assets. Content-addressed font filenames in the theme registry ensure that two themes sharing the +same font end up with one byte payload on disk. +-/ +def writeThemeAssets (dir : System.FilePath) (config : RenderConfig) + (codeSampleHtml : String) : EmitM Unit := do + let themes ← readThe ThemeRegistry + ensureDir (dir / "-verso-data") + -- verso-themes.css + withFile (dir / "verso-themes.css") .write fun h => do + h.putStrLn (Theme.«verso-themes.css» themes + config.defaultLightTheme config.defaultDarkTheme config.defaultAppearance) + -- Font bytes, deduplicated by output path: a theme's @font-face rules embed the per-theme + -- asset-root path, so writing one path and skipping a structurally-identical-bytes path under + -- a different theme root would leave that rule pointing at a missing file. + let mut writtenPaths : Std.HashSet String := {} + for (n, t) in themes do + let assetRoot := s!"-verso-data/themes/{n.toString}" + for (path, bytes, _, _) in t.fontAssets assetRoot do + if writtenPaths.contains path then continue + writtenPaths := writtenPaths.insert path + let abs := dir.join path + if let some p := abs.parent then ensureDir p + writeBinFile abs bytes + -- Theme-bundled assets (images, etc.). Defensively skip any asset whose path is unsafe + -- (`..` segments, leading/trailing/double `/`, backslashes) — the validation pass logs an + -- `unsafeAssetPath` error for these, but build-log errors are non-fatal and the build + -- continues into emission, so the writer must independently refuse to honor the bad path. + -- Without this guard a malicious or buggy theme could clobber files outside its asset root + -- via a path like `../../book.css`. + for (n, t) in themes do + for a in t.assets do + unless Theme.ThemeAsset.safePath a.path do + Verso.reportError + s!"refusing to write theme asset for '{n.toString}': unsafe path '{a.path}'" + continue + let path := dir / "-verso-data" / "themes" / n.toString / a.path + if let some p := path.parent then ensureDir p + writeBinFile path a.contents + -- Picker assets + data file. + writeFile (dir / "-verso-data" / "theme-picker.js") Manual.Theme.«theme-picker.js» + writeFile (dir / "-verso-data" / "theme-picker.css") Manual.Theme.«theme-picker.css» + writeFile (dir / "-verso-data" / "verso-themes.js") + (Theme.windowVersoThemesJs themes config.defaultLightTheme config.defaultDarkTheme + config.defaultAppearance codeSampleHtml) + +open IO.FS in +def emitTeX (config : RenderConfig) (text : Part Manual) : EmitM Unit := do + let (text, state) ← traverse text config.toConfig let opts : TeX.Options Manual := { headerLevels := #["chapter", "section", "subsection", "subsubsection", "paragraph"], headerLevel := some ⟨0, by grind⟩ @@ -395,7 +510,7 @@ def emitTeX (config : Config) (text : Part Manual) : EmitM Unit := do withFile (dir.join "main.tex") .write fun h => do if config.verbose then IO.println s!"Saving {dir.join "main.tex"}" - h.putStrLn (preamble text.titleString authors date packages.toList preambleItems.toList) + h.putStrLn (preamble text.titleString authors date packages.toList preambleItems.toList config.pdfCodeTheme) -- \frontmatter is inserted by our hardcoded preamble before the ToC, so it doesn't get inserted -- here. If there's any text at the start of the front matter, then we need to clear it to a new -- recto page after the ToC @@ -482,7 +597,8 @@ def page (toc : List Html.Toc) (state : TraverseState) (config : Config) (localItems : Array Html) (showNavButtons : Bool := true) (extraJs : List JS := []) - (extraHead : Html := .empty) : Html := + (extraHead : Html := .empty) + (themeInitScript : String := "") (showThemePicker : Bool := false) : Html := let toc := { title := htmlBookTitle, path := #[], id := "" , sectionNum := some #[], children := toc } @@ -504,6 +620,7 @@ def page (toc : List Html.Toc) state.extraCss (state.extraJs.insertMany extraJs) (showNavButtons := showNavButtons) (logo := config.logo) + (logoDark := config.logoDark) (logoLink := config.logoLink) (repoLink := config.sourceLink) (issueLink := config.issueLink) @@ -512,6 +629,8 @@ def page (toc : List Html.Toc) (extraJsFiles := featureJsFiles ++ extraJsFiles) (extraHead := config.extraHead |>.push extraHead) (extraContents := config.extraContents) + (themeInitScript := themeInitScript) + (showThemePicker := showThemePicker) def relativizeLinks (html : Html) : Html := -- Make all absolute URLS be relative to the site root, because that'll make them ``-relative @@ -716,7 +835,8 @@ def emitHtmlSingle emitSearchBox (dir / "-verso-search") state.quickJump config.searchPriorities (searchPagePath := some "search/") emitSearchIndex (dir / "-verso-search") state { draft := config.draft } text where - emitContent (dir : System.FilePath) : StateT (State Html) (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))) Unit := do + emitContent (dir : System.FilePath) : StateT (State Html) (ReaderT AllRemotes EmitM) Unit := do + let registry ← readThe ThemeRegistry let authors := text.metadata.map (·.authors) |>.getD [] let authorshipNote := text.metadata.bind (·.authorshipNote) let _date := text.metadata.bind (·.date) |>.getD "" -- TODO @@ -758,10 +878,18 @@ where emitFindHtml toc dir state xrefJson config.toConfig if .search ∈ config.features then emitSearchResultsHtml toc dir titleToShow state config.toConfig - IO.FS.withFile (dir.join "verso-vars.css") .write fun h => do - h.putStrLn Html.«verso-vars.css» IO.FS.withFile (dir.join "book.css") .write fun h => do h.putStrLn Html.Css.pageStyle + -- Render the picker preview against the in-progress hover state so its `data-verso-hover` + -- IDs end up in the global `-verso-docs.json` the page loads — the same lookup the picker + -- JS already does for every other token. Without this the picker tokens have hover IDs + -- that reference nothing. + let codeSampleCtx : Verso.Code.HighlightHtmlM.Context Manual := { + linkTargets := {}, traverseContext := {}, definitionIds := {}, options := {} + } + let (codeSampleHtml, htmlState') := Manual.Theme.codeSampleHtml codeSampleCtx (← get) + set htmlState' + writeThemeAssets dir config codeSampleHtml for (src, dest) in config.extraFiles do copyRecursively src (dir.join dest) for (src, dest) in config.extraFilesHtml do @@ -778,8 +906,19 @@ where if config.verbose then IO.println s!"Saving {dir.join "index.html"}" h.putStrLn Html.doctype + -- Offer the picker only when the reader has a real choice. A registry with one entry + -- (or none) means the unscoped `:root` block already paints the only available theme. + let showThemePicker := registry.size > 1 + let themeInitScript := + if showThemePicker then + Verso.Theme.themeInitScript registry + config.defaultLightTheme config.defaultDarkTheme config.defaultAppearance + else "" h.putStrLn <| Html.asString <| relativizeLinks <| - page toc ctxt.path text.titleString titleToShow pageContent state config.toConfig thisPageToc (showNavButtons := false) + page toc ctxt.path text.titleString titleToShow pageContent state config.toConfig thisPageToc + (showNavButtons := false) + (themeInitScript := themeInitScript) + (showThemePicker := showThemePicker) /-- @@ -810,7 +949,7 @@ where Emits the data used by all pages in the site, such as JS and CSS, and then emits the root page (and thus its children). -/ - emitContent (root : System.FilePath) : StateT (State Html) (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))) Unit := do + emitContent (root : System.FilePath) : StateT (State Html) (ReaderT AllRemotes EmitM) Unit := do let authors := text.metadata.map (·.authors) |>.getD [] let authorshipNote := text.metadata >>= (·.authorshipNote) let _date := text.metadata.bind (·.date) |>.getD "" -- TODO @@ -826,10 +965,18 @@ where if let some alt := text.metadata.bind (·.shortTitle) then alt else titleHtml - IO.FS.withFile (root / "verso-vars.css") .write fun h => do - h.putStrLn Html.«verso-vars.css» IO.FS.withFile (root / "book.css") .write fun h => do h.putStrLn Html.Css.pageStyle + -- Render the picker preview against the in-progress hover state so its `data-verso-hover` + -- IDs end up in the global `-verso-docs.json` the page loads — the same lookup the picker + -- JS already does for every other token. Without this the picker tokens have hover IDs + -- that reference nothing. + let codeSampleCtx : Verso.Code.HighlightHtmlM.Context Manual := { + linkTargets := {}, traverseContext := {}, definitionIds := {}, options := {} + } + let (codeSampleHtml, htmlState') := Manual.Theme.codeSampleHtml codeSampleCtx (← get) + set htmlState' + writeThemeAssets root config codeSampleHtml for (src, dest) in config.extraFiles do copyRecursively src (root.join dest) for (src, dest) in config.extraFilesHtml do @@ -847,7 +994,8 @@ where -/ emitPart (bookTitle : Html) (authors : List String) (authorshipNote : Option String) (bookContents) (opts ctxt state definitionIds linkTargets codeOptions) - (root : Bool) (depth : Nat) (dir : System.FilePath) (part : Part Manual) : StateT (State Html) (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))) Unit := do + (root : Bool) (depth : Nat) (dir : System.FilePath) (part : Part Manual) : StateT (State Html) (ReaderT AllRemotes EmitM) Unit := do + let registry ← readThe ThemeRegistry let thisFile := part.metadata.bind (·.file) |>.getD (part.titleString.sluggify.toString) let dir := if root then dir else dir.join thisFile let sectionNum := sectionHtml ctxt @@ -898,8 +1046,18 @@ where if config.verbose then IO.println s!"Saving {dir.join "index.html"}" h.putStrLn Html.doctype + -- Offer the picker only when the reader has a real choice. A registry with one entry + -- (or none) means the unscoped `:root` block already paints the only available theme. + let showThemePicker := registry.size > 1 + let themeInitScript := + if showThemePicker then + Verso.Theme.themeInitScript registry + config.defaultLightTheme config.defaultDarkTheme config.defaultAppearance + else "" h.putStrLn <| Html.asString <| relativizeLinks <| page bookContents ctxt.path part.titleString bookTitle pageContent state config.toConfig thisPageToc + (themeInitScript := themeInitScript) + (showThemePicker := showThemePicker) if depth > 0 ∧ part.htmlSplit != .never then for p in part.subParts do let nextFile := p.metadata.bind (·.file) |>.getD (p.titleString.sluggify.toString) @@ -944,10 +1102,13 @@ open Verso.CLI def manualMain (text : Part Manual) (extensionImpls : ExtensionImpls := by exact extension_impls%) + (codeThemes : Verso.Theme.CodeThemeTable := by exact code_themes%) + (manualThemes : Verso.Theme.ManualThemeTable := by exact manual_themes%) (options : List String) (config : RenderConfig := {}) (extraSteps : List ExtraStep := []) : IO UInt32 := - ReaderT.run go extensionImpls + let _ := codeThemes + go extensionImpls manualThemes where @@ -998,21 +1159,122 @@ where fixBase (base : String) : String := if base.endsWith "/" then base else base ++ "/" - go (extensionImpls : ExtensionImpls) : IO UInt32 := do + /-- + Runs the theme set's accessibility checks at three tiers: + + - **Coverage** (gated by + `strictThemeCoverage`): + the build must offer a usable theme. With a single registered theme it must be accessible; + with multiple themes at least one accessible light *and* one accessible dark must exist. + + - **Default theme** (gated by + `strictDefaultThemeAccessibility`): + the configured `defaultLightTheme` + and `defaultDarkTheme` + must themselves be accessible. + + - **Per-theme advisory** (gated by + `warnPerThemeAccessibility`): + every registered theme with any accessibility issues emits a build-log warning naming the + theme and the specific issues. + + A theme counts as "accessible" iff its + `ManualTheme.checkAccessibility` returns no issues. + -/ + runThemeAccessibilityCheck (cfg : RenderConfig) (registry : ThemeRegistry) : + ReaderT ExtensionImpls (BuildLogT IO) Unit := do + let issuesOf (t : Verso.Theme.ManualTheme) := t.checkAccessibility + let isAccessible (t : Verso.Theme.ManualTheme) : Bool := (issuesOf t).isEmpty + -- Per-theme advisory. + if cfg.warnPerThemeAccessibility then + for (n, t) in registry do + for issue in issuesOf t do + let colors := issue.offending.toList.map Verso.Theme.Color.css |> ", ".intercalate + let suffix := if colors.isEmpty then "" else s!" ({colors})" + Verso.reportWarning s!"theme '{n.toString}' ({t.name}): {issue.message}{suffix}" + -- Coverage. + let routeCoverage (msg : String) : ReaderT ExtensionImpls (BuildLogT IO) Unit := + if cfg.strictThemeCoverage then Verso.reportError msg else Verso.reportWarning msg + let accessible := registry.filter (fun _ t => isAccessible t) + if accessible.isEmpty then + routeCoverage "no registered theme is accessible; readers cannot pick a usable theme" + else if registry.size > 1 then + let anyLight := accessible.any (fun _ t => t.appearance == Verso.Theme.Appearance.light) + let anyDark := accessible.any (fun _ t => t.appearance == Verso.Theme.Appearance.dark) + unless anyLight do + routeCoverage "no registered light theme is accessible; readers on a light system cannot pick a usable theme" + unless anyDark do + routeCoverage "no registered dark theme is accessible; readers on a dark system cannot pick a usable theme" + -- Default theme accessibility. + let routeDefault (msg : String) : ReaderT ExtensionImpls (BuildLogT IO) Unit := + if cfg.strictDefaultThemeAccessibility then Verso.reportError msg else Verso.reportWarning msg + let checkDefault (slot : String) (name : Lean.Name) : + ReaderT ExtensionImpls (BuildLogT IO) Unit := do + match registry.find? name with + | none => pure () -- already reported by validate + | some t => + let issues := issuesOf t + unless issues.isEmpty do + let plural := if issues.size == 1 then "" else "s" + let lines := issues.toList.map fun i => + let colors := i.offending.toList.map Verso.Theme.Color.css |> ", ".intercalate + let suffix := if colors.isEmpty then "" else s!" ({colors})" + s!" - {i.message}{suffix}" + let body := "\n".intercalate lines + routeDefault + s!"{slot} '{name.toString}' ({t.name}) has {issues.size} accessibility issue{plural}:\n{body}" + checkDefault "defaultLightTheme" cfg.defaultLightTheme + checkDefault "defaultDarkTheme" cfg.defaultDarkTheme + + /-- + Builds the active {name}`ThemeRegistry` from the registered + `ManualTheme` table, filters it by the configured + `availableThemes`, and routes every + `ManualThemeTable.ValidationError` through `MonadBuildLog` as an error. + -/ + resolveThemeRegistry (cfg : RenderConfig) + (table : Verso.Theme.ManualThemeTable) : + ReaderT ExtensionImpls (BuildLogT IO) ThemeRegistry := do + for e in table.validate cfg.defaultLightTheme cfg.defaultDarkTheme cfg.availableThemes do + Verso.reportError e.format + -- `availableThemes` semantics: + -- `none` → every registered theme is available + -- `some [..xs]` → exactly those themes, with `defaultLightTheme` and + -- `defaultDarkTheme` implicitly added if missing so the picker always + -- contains the resolved default for each appearance. + -- The result always contains at least `defaultLightTheme` and `defaultDarkTheme` if those + -- are registered, so `verso-themes.css` always has a light and a dark default to fall back + -- to for readers without JavaScript. + match cfg.availableThemes with + | none => return table.themes + | some xs => + let withDefaults := xs + |>.append (if xs.contains cfg.defaultLightTheme then {} else {cfg.defaultLightTheme}) + |>.append (if xs.contains cfg.defaultDarkTheme then {} else {cfg.defaultDarkTheme}) + return withDefaults.foldl (init := ({} : ThemeRegistry)) fun acc n => + match table.find? n with + | some t => acc.insert n t + | none => acc + + go (extensionImpls : ExtensionImpls) (manualThemes : Verso.Theme.ManualThemeTable) : IO UInt32 := do let cfg ← opts config options runWithLogger <| flip ReaderT.run extensionImpls do - if cfg.emitTeX then - if cfg.verbose then - IO.println s!"Saving TeX" - emitTeX cfg.toConfig text - - emitHtml cfg.emitHtmlSingle .single cfg text traverseHtmlSingle emitHtmlSingle - emitHtml cfg.emitHtmlMulti .multi cfg text traverseHtmlMulti emitHtmlMulti - - if let some wcFile := cfg.wordCount then - if cfg.verbose then - IO.println s!"Saving word counts to {wcFile}" - wordCount wcFile cfg.toConfig text + let registry ← resolveThemeRegistry cfg manualThemes + runThemeAccessibilityCheck cfg registry + let body : EmitM Unit := do + if cfg.emitTeX then + if cfg.verbose then + IO.println s!"Saving TeX" + emitTeX cfg text + + emitHtml cfg.emitHtmlSingle .single cfg text traverseHtmlSingle emitHtmlSingle + emitHtml cfg.emitHtmlMulti .multi cfg text traverseHtmlMulti emitHtmlMulti + + if let some wcFile := cfg.wordCount then + if cfg.verbose then + IO.println s!"Saving word counts to {wcFile}" + wordCount wcFile cfg.toConfig text + body.run registry emitHtml (how : EmitHtml) (mode : Mode) (cfg : RenderConfig) (text : Part Manual) diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index f40cf1f54..50ecf67cb 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/src/verso-manual/VersoManual/Basic.lean @@ -7,6 +7,7 @@ module import Std.Data.HashSet import Std.Data.TreeSet import Verso.Doc +public import Verso.Font public import Verso.Instances public import Verso.Doc.Html public import Verso.Doc.TeX @@ -19,6 +20,7 @@ public import VersoSearch.DomainSearch import VersoManual.LicenseInfo import VersoManual.Html.Config public import VersoManual.Html.Features +public import VersoManual.Theme public meta import VersoManual.Ext import Verso.Output.Html public import Verso.Output.TeX @@ -83,16 +85,8 @@ def toCss (family : FontFamily) : String := s!"font-family: var({family.toCssVar end FontFamily -inductive FontStyle where - | normal - | italic -deriving DecidableEq, Repr, Hashable - -def FontStyle.toCss (s : FontStyle) : String := - "font-style: " ++ - match s with - | .normal => "normal;" - | .italic => "italic;" +-- `FontStyle` was previously defined here; it is re-exported here for backwards compatibility +export Verso (FontStyle) inductive FontWeight where | lighter @@ -682,6 +676,26 @@ structure ExtensionImpls where inlineDescrs : Lean.NameMap Dynamic blockDescrs : Lean.NameMap Dynamic +/-- +{open Verso.Theme} + +The monad in which TeX descriptor implementations (`BlockDescr.toTeX`, `InlineDescr.toTeX`) and the +TeX generation pipeline run. Reads the resolved {name}`ThemeRegistry`, the extension implementations +table, and logs through the build log. + +Defined here (not in `VersoManual.lean`) so descriptor type signatures can name it without forward +references. +-/ +public abbrev EmitM : Type → Type := + ReaderT Verso.Theme.ThemeRegistry (ReaderT Manual.ExtensionImpls (BuildLogT IO)) + +/-- +The monad in which HTML descriptor implementations (`BlockDescr.toHtml`, `InlineDescr.toHtml`) run. +Same as {name}`EmitM`, with the remote cross-reference table read in addition. +-/ +public abbrev EmitHtmlM : Type → Type := + ReaderT Multi.AllRemotes EmitM + end Manual /-- A genre for writing reference manuals and other book-like documents. -/ @@ -759,7 +773,7 @@ structure InlineDescr extends HtmlAssets where /-- How to generate HTML. If {name}`none`, generating HTML from a document that contains this inline will fail. -/ - toHtml : Option (InlineToHtml Manual (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO)))) + toHtml : Option (InlineToHtml Manual EmitHtmlM) /-- Should this inline be an entry in the page-local ToC? If so, how should it be represented? @@ -778,7 +792,7 @@ structure InlineDescr extends HtmlAssets where How to generate TeX. If {name}`none`, generating TeX from a document that contains this inline will fail. -/ - toTeX : Option (InlineToTeX Manual (ReaderT ExtensionImpls (BuildLogT IO))) + toTeX : Option (InlineToTeX Manual EmitM) /-- Required TeX `\usepackage` lines -/ usePackages : List String := {} /-- Required items in the TeX preamble -/ @@ -802,7 +816,7 @@ structure BlockDescr extends HtmlAssets where How to generate HTML. If {name}`none`, generating HTML from a document that contains this block will fail. -/ - toHtml : Option (BlockToHtml Manual (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO)))) + toHtml : Option (BlockToHtml Manual EmitHtmlM) /-- Should this block be an entry in the page-local ToC? If so, how should it be represented? @@ -822,7 +836,7 @@ structure BlockDescr extends HtmlAssets where How to generate TeX. If {name}`none`, generating TeX from a document that contains this block will fail. -/ - toTeX : Option (BlockToTeX Manual (ReaderT ExtensionImpls (BuildLogT IO))) + toTeX : Option (BlockToTeX Manual EmitM) /-- Required TeX `\usepackage` lines -/ usePackages : List String := {} /-- Required items in the TeX preamble -/ @@ -1512,7 +1526,7 @@ instance : Traverse Manual TraverseM where pure <| some <| Inline.other ⟨name, some id, data⟩ content open Verso.Output.TeX in -instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls (BuildLogT IO)) where +instance : TeX.GenreTeX Manual EmitM where part go metadata txt := do let st ← TeX.state let label? := do @@ -1574,7 +1588,7 @@ def permalink (id : InternalId) (st : TraverseState) (inline : Bool := true) : H open Verso.Output.Html in -instance : Html.GenreHtml Manual (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))) where +instance : Html.GenreHtml Manual EmitHtmlM where part go «meta» txt := do let st ← Verso.Doc.Html.HtmlT.state let attrs := meta.id.map (st.htmlId) |>.getD #[] diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean index 0510112e1..680129901 100644 --- a/src/verso-manual/VersoManual/Bibliography.lean +++ b/src/verso-manual/VersoManual/Bibliography.lean @@ -205,7 +205,7 @@ where open Verso.Doc.TeX in open Verso.Output.TeX in -def Citable.bibTeX (go : Doc.Inline Genre.Manual → TeXT Manual (ReaderT ExtensionImpls (BuildLogT IO)) TeX) (c : Citable) : TeXT Manual (ReaderT ExtensionImpls (BuildLogT IO)) TeX := wrap <$> open TeX in do +def Citable.bibTeX (go : Doc.Inline Genre.Manual → TeXT Manual (EmitM) TeX) (c : Citable) : TeXT Manual (EmitM) TeX := wrap <$> open TeX in do match c with | .inProceedings p => let authors ← andListTeX <$> p.authors.mapM go @@ -288,10 +288,10 @@ where open Verso.Doc.TeX in def Citable.inlineTeX - (go : Doc.Inline Genre.Manual → TeXT Manual (ReaderT ExtensionImpls (BuildLogT IO)) Output.TeX) + (go : Doc.Inline Genre.Manual → TeXT Manual (EmitM) Output.TeX) (ps : List Citable) (fmt : Style) : - TeXT Manual (ReaderT ExtensionImpls (BuildLogT IO)) TeX := open TeX in do + TeXT Manual (EmitM) TeX := open TeX in do match fmt with | .textual => let out : Array TeX ← ps.toArray.mapM fun p => do diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index 9d5d54892..3b8e10ffa 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -418,11 +418,14 @@ public def page (extraContents : Array Html := #[]) (showNavButtons : Bool := true) (logo : Option String := none) + (logoDark : Option String := none) (logoLink : Option String := none) (repoLink : Option String := none) (issueLink : Option String := none) (extraStylesheets : List String := []) - (extraJsFiles : Array (String × Bool) := #[]) : Html := + (extraJsFiles : Array (String × Bool) := #[]) + (themeInitScript : String := "") + (showThemePicker : Bool := false) : Html := let relativeRoot := String.join <| "./" :: path.toList.map (fun _ => "../") let defer := #[("defer", "defer")] {{ @@ -435,8 +438,19 @@ public def page {{textTitle}} + {{if themeInitScript.isEmpty then .empty else + {{}} }} - + + {{if showThemePicker then + {{}} + else .empty }} + {{if showThemePicker then + {{}} + else .empty }} + {{if showThemePicker then + {{}} + else .empty }} {{ searchAssetTags }} {{extraJsFiles.map fun f => ({{}})}} @@ -449,16 +463,30 @@ public def page
{{if let some url := logo then - let logoHtml := {{}} let logoDest := if let some root := logoLink then root else "/" - {{}} + let lightImg := + if logoDark.isSome then + {{}} + else + {{}} + let darkImg := + if let some d := logoDark then {{}} + else .empty + {{}} else .empty }}

{{bookTitle}}
+ {{if showThemePicker then + {{
+ +
}} + else .empty }}