feat: add dark mode support via prefers-color-scheme by alok · Pull Request #676 · leanprover/verso

alok · 2025-12-16T08:32:34Z

Summary

Add automatic dark mode support that respects operating system preferences using the @media (prefers-color-scheme: dark) CSS media query.

Add new CSS custom properties for backgrounds, borders, links, shadows, and message colors
verso-vars.css now includes dark mode variants that automatically activate based on OS preference
Updated all CSS files (code.css, search-box.css, search-highlight.css) to use CSS variables instead of hardcoded colors
Updated Style.lean to use CSS variables throughout

The color scheme is harmonized with lean-lang.org as requested:

Light mode: #ffffff background, #333 text, #386ee0 links, #f9fbfd surface
Dark mode: #1e1e1e background, #eee text, #3b94ff links, #181818 surface

Test plan

Build the project (lake build)
Generate sample documentation and verify light mode appearance
Toggle OS dark mode preference and verify dark mode appearance
Check that colors harmonize with lean-lang.org in both modes
Test on mobile viewport sizes

Closes #641

Add automatic dark mode support that respects operating system preferences using the `@media (prefers-color-scheme: dark)` CSS media query. Changes: - verso-vars.css: Add new CSS custom properties for backgrounds, borders, links, shadows, and message colors with dark mode variants - code.css: Update API docs styling to use CSS variables - search-box.css/search-highlight.css: Update search UI to use CSS variables - Style.lean: Update manual page styling to use CSS variables The color scheme is harmonized with lean-lang.org: - Light: #ffffff background, leanprover#333 text, #386ee0 links - Dark: #1e1e1e background, #eee text, #3b94ff links Closes leanprover#641

david-christiansen · 2025-12-16T09:46:14Z

This sounds great, and looks good based on the diffs!

Given that you've got a checklist, I'll hold off on reviewing it until you indicate that you're ready. WRT testing the dark mode toggle, we do have Playwright tests for some features already, which seems like a natural place to put these tests.

alok · 2025-12-17T11:44:16Z

Thanks for the feedback! I've fixed the prettier formatting issue that was causing CI to fail.

The core dark mode via @media (prefers-color-scheme: dark) is complete and working. I also added:

A manual theme toggle button (sun/moon icons) with localStorage persistence
Support for data-theme="light|dark" attribute override for users who want to override their OS preference
Theme toggle JavaScript that cycles through: system → dark → light → system

For testing the dark mode toggle, I can add Playwright tests. Should I:

Add tests for the theme toggle button functionality (clicking cycles themes, localStorage persistence)?
Add visual regression tests comparing light vs dark mode appearance?
Both?

david-christiansen · 2026-01-05T15:33:31Z

Sorry for the delay in replying. Winter holidays are now over!

I think that Playwright tests for the toggle button are important, because local storage won't be "automatically" tested in any reasonable way by most daily use of the sites, and issues would affect first-time readers disproportionately. I think the risk of regressions on the visual aspects is relatively small, though. So number 1 :-)

Thanks again, this is really a wonderful improvement!

david-christiansen · 2026-01-05T15:56:58Z

A few specific comments. Aside from these, this is great to read! I think the truly critical one is the missing JS.

Search Box Contrast

Here, I have a hard time seeing the border of the search box on my screen:

Can the dark-mode box be made more distinct?

Toggle Script 404

I get a 404 for localhost:8800/theme-toggle.js . Is this not placed where it should be in the generated code?

Tags Very Bright

The "structure" tag in this rendering has a light background, and seems very bright compared to the rest of the page. What's your thought process behind this decision?

david-christiansen · 2026-01-06T05:32:37Z

static-web/verso-vars.css


+    /** Background colors **/
+    --verso-background-color: #ffffff;
+    --verso-surface-color: #f9fbfd;


A comment here explaining the "surface" terminology would be helpful.

Added in 5837227. I documented "surface" directly above --verso-surface-color in static-web/verso-vars.css as the secondary/elevated background for controls and sidebars.

Thanks for the comment!

I'm still not wild about this terminology, even with the explanatory comment - surface immediately makes my brain want to think about graphics contexts and drawing APIs and the like, not regions of webpages. What about calling it --verso-secondary-background-color?

static-web/verso-vars.css

alok · 2026-02-10T09:16:51Z

Addressed the remaining dark-mode feedback in 3 commits now pushed:\n\n- 5837227\n - Made dark mode opt-in via data-verso-dark-mode in static-web/verso-vars.css and set that attribute in the manual HTML backend.\n - Added explanatory comment for the surface color token.\n - Fixed theme-toggle.js 404 by emitting the file in generated manual output and wiring it as a tracked input asset.\n- af1ee87\n - Increased search-box contrast in dark mode with dedicated border vars and stronger border styling.\n - Made docstring labels/theme badges inherit theme-aware colors (removed hardcoded bright values).\n- e47250b\n - Added Playwright tests for theme toggle cycling + localStorage persistence (browser-tests/test_dark_mode.py).\n\nI also replied to and resolved the two open review threads.

alok · 2026-02-10T23:17:53Z

Pushed one more follow-up commit (c969c1a) for dark mode polish:

fixed a hover-message CSS override so error/info hover tooltips stay theme-aware in dark mode
fixed header interaction where the search box layer could intercept clicks on #theme-toggle
validated with full usersguide generation + Playwright dark-mode tests (10 passed)

Please take another look when convenient.

david-christiansen · 2026-02-11T23:28:33Z

Thanks, I'll give it a look when I can. I'm on vacation until Monday, and will be away from computers until then :-)

david-christiansen · 2026-02-11T23:28:51Z

In the meantime there's a couple of merge conflicts...

github-actions · 2026-02-20T19:12:26Z

Preview for this PR is ready! 🎉

david-christiansen · 2026-02-20T19:20:05Z

OK, the previews for the PRs are working again. It's looking like it works now - I'll get into details ASAP. Thanks for your patience!

david-christiansen · 2026-02-20T19:30:38Z

static-web/verso-vars.css

+}
+
+/** Manual dark mode override **/
+:root[data-verso-dark-mode][data-theme="dark"] {


This section is a duplicate of the variables above, right? How do we keep them in sync?

david-christiansen · 2026-02-20T19:32:51Z

static-web/theme-toggle.js

+            "aria-label",
+            effective === "dark" ? "Switch to light mode" : "Switch to dark mode",
+        );
+        toggle.innerHTML = effective === "dark" ? "☀️" : "🌙";


I'm a bit concerned about emoji as UI elements. They can look very different in different places, and their color is a bit out of place. Can we use some standard SVG icons here? Maybe the one from lean-lang.org?

Also, when clicking through the page, I had a hard time figuring out the workflow for getting back to the system theme. How should users do that?

david-christiansen · 2026-02-20T19:36:55Z

I'm not sure where to put it, but this should probably also set the color-scheme property, right?

david-christiansen · 2026-02-20T19:38:44Z

static-web/search/search-box.css

    position: absolute;
    top: 0;
-    right: 0;
+    right: 3rem;


This feels like a fragile way to make space. What about some kind of flexbox wrapper into which the search box and toggle widget are placed that can manage them well, also if we add another widget there in the future?

david-christiansen · 2026-02-20T19:43:26Z

static-web/verso-vars.css

+        --verso-link-hover-color: #4d9efc;
+
+        /** Border colors **/
+        --verso-border-color: #4c4c4c;


The contrast ratio between 4c4c4c and 1e1e1e is 1.94:1 according to https://webaim.org/resources/contrastchecker/ . WCAG wants 3:1 for interface components, which would put the border at #696969 according to that site. What do you think about this solution?

david-christiansen · 2026-02-20T19:45:58Z

Thanks a bunch, once again!

alok force-pushed the feature/dark-mode-support branch from 2d3bac6 to 3d68642 Compare December 16, 2025 08:38

alok force-pushed the feature/dark-mode-support branch from 3d68642 to be4f660 Compare December 16, 2025 08:49

style: apply prettier formatting to theme-toggle.js

ba2c0ea

david-christiansen reviewed Jan 6, 2026

View reviewed changes

static-web/verso-vars.css Show resolved Hide resolved

alok added 3 commits February 10, 2026 00:40

fix: make dark mode opt-in and emit theme toggle asset

5837227

fix: improve dark-mode contrast for search and doc labels

af1ee87

test: add playwright coverage for dark-mode toggle state

e47250b

alok added 4 commits February 10, 2026 01:24

test: verify theme toggle asset is served

0cc855c

test: verify dark styles are gated by opt-in attribute

9346c5b

test: cover dark-system light override path

3723d51

Fix dark mode hover styling and theme toggle header overlap

c969c1a

david-christiansen and others added 3 commits February 20, 2026 17:02

Merge remote-tracking branch 'upstream/main' into dark-mode-merge-main

68d5ffb

Merge branch 'main' into feature/dark-mode-support

67149b0

Merge branch 'main' into feature/dark-mode-support

e93a221

david-christiansen reviewed Feb 20, 2026

View reviewed changes

Conversation

alok commented Dec 16, 2025

Summary

Test plan

Uh oh!

david-christiansen commented Dec 16, 2025

Uh oh!

alok commented Dec 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

david-christiansen commented Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

david-christiansen commented Jan 5, 2026

Search Box Contrast

Toggle Script 404

Tags Very Bright

Uh oh!

david-christiansen Jan 6, 2026

Choose a reason for hiding this comment

Uh oh!

alok Feb 10, 2026

Choose a reason for hiding this comment

Uh oh!

david-christiansen Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

alok commented Feb 10, 2026

Uh oh!

alok commented Feb 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

david-christiansen commented Feb 11, 2026

Uh oh!

david-christiansen commented Feb 11, 2026

Uh oh!

github-actions bot commented Feb 20, 2026

Uh oh!

david-christiansen commented Feb 20, 2026

Uh oh!

david-christiansen Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

david-christiansen Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

david-christiansen commented Feb 20, 2026

Uh oh!

david-christiansen Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

david-christiansen Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

david-christiansen commented Feb 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

alok commented Dec 17, 2025 •

edited

Loading

david-christiansen commented Jan 5, 2026 •

edited

Loading

alok commented Feb 10, 2026 •

edited

Loading