add colorscheme toggle

DocGen4/Output.lean

@@ -40,6 +40,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let docGenStatic := #[
     ("style.css", styleCss),
     ("declaration-data.js", declarationDataCenterJs),
+    ("color-scheme.js", colorSchemeJs),
     ("nav.js", navJs),
     ("how-about.js", howAboutJs),
     ("search.html", searchHtml),

DocGen4/Output/Base.lean

@@ -148,6 +148,7 @@ are used in documentation generation, notably JS and CSS ones.
 -/
   def styleCss : String := include_str "../../static/style.css"
   def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
+  def colorSchemeJs : String := include_str "../../static/color-scheme.js"
   def navJs : String := include_str "../../static/nav.js"
   def howAboutJs : String := include_str "../../static/how-about.js"
   def searchJs : String := include_str "../../static/search.js"

DocGen4/Output/Navbar.lean

@@ -62,6 +62,7 @@ def navbar : BaseHtmlM Html := do
         [← baseHtmlHeadDeclarations]
 
         <script type="module" src={s!"{← getRoot}nav.js"}></script>
+        <script type="module" src={s!"{← getRoot}color-scheme.js"}></script>
         <base target="_parent" />
       </head>
 
@@ -82,6 +83,18 @@ def navbar : BaseHtmlM Html := do
           -/
           <h3>Library</h3>
           {← moduleList}
+          <div id="settings">
+            -- `input` is a void tag, but can be self-closed to make parsing easier.
+            <h3>Color scheme</h3>
+            <form id="color-theme-switcher">
+                <label for="color-theme-dark">
+                    <input type="radio" name="color_theme" id="color-theme-dark" value="dark" autocomplete="off"/>dark</label>
+                <label for="color-theme-system" title="Match system theme settings">
+                    <input type="radio" name="color_theme" id="color-theme-system" value="system" autocomplete="off"/>system</label>
+                <label for="color-theme-light">
+                    <input type="radio" name="color_theme" id="color-theme-light" value="light" autocomplete="off"/>light</label>
+            </form>
+          </div>
         </nav>
         </div>
       </body>

DocGen4/Process/Hierarchy.lean

@@ -84,6 +84,7 @@ partial def fromArray (names : Array Name) : Hierarchy :=
 def baseDirBlackList : HashSet String :=
   HashSet.fromArray #[
     "404.html",
+    "color-scheme.js",
     "declaration-data.js",
     "declarations",
     "find",

lakefile.lean

@@ -85,6 +85,7 @@ library_facet docs (lib) : FilePath := do
   let staticFiles := #[
     basePath / "style.css",
     basePath / "declaration-data.js",
+    basePath / "color-scheme.js",
     basePath / "nav.js",
     basePath / "how-about.js",
     basePath / "search.js",

static/color-scheme.js

@@ -0,0 +1,28 @@
+function getTheme() {
+    return localStorage.getItem("theme") || "system";
+}
+
+function setTheme(themeName) {
+    localStorage.setItem('theme', themeName);
+    if (themeName == "system") {
+        themeName = window.matchMedia("(prefers-color-scheme: dark)").matches ? "dark" : "light";
+    }
+    // the navbar is in an iframe, so we need to set this variable in the parent document
+    parent.document.documentElement.setAttribute('data-theme', themeName);
+}
+
+setTheme(getTheme())
+
+document.addEventListener("DOMContentLoaded", function() {
+    document.querySelectorAll("#color-theme-switcher input").forEach((input) => {
+        if (input.value == getTheme()) {
+            input.checked = true;
+        }
+        input.addEventListener('change', e => setTheme(e.target.value));
+    });
+
+    // also check to see if the user changes their theme settings while the page is loaded.
+    window.matchMedia('(prefers-color-scheme: dark)').addEventListener('change', event => {
+        setTheme(getTheme());
+    })
+});

static/style.css

@@ -22,7 +22,6 @@ body { line-height: 1.5; }
 nav { line-height: normal; }
 
 :root {
-    color-scheme: light;
     --header-height: 3em;
     --fragment-offset: calc(var(--header-height) + 1em);
     --content-width: 55vw;
@@ -54,8 +53,37 @@ nav { line-height: normal; }
     --fragment-offset: calc(var(--header-height) + 1em);
     --content-width: 55vw;
 }
+
+/* automatic dark theme if no javascript */
 @media (prefers-color-scheme: dark) {
     :root {
+        --header-bg: #111010;
+        --body-bg: #171717;
+        --code-bg: #363333;
+        --text-color: #eee;
+        --link-color: #58a6ff;
+
+        --implicit-arg-text-color: var(--text-color);
+
+        --def-color: #1F497F;
+        --def-color-hsl-angle: 214;
+        --theorem-color: #134E2D;
+        --theorem-color-hsl-angle: 146;
+        --axiom-and-constant-color: #6B1B1A;
+        --axiom-and-constant-color-hsl-angle: 1;
+        --structure-and-inductive-color: #73461C;
+        --structure-and-inductive-color-hsl-angle: 29;
+        --starting-percentage: 30;
+
+        --hamburger-bg-color: #2d2c2c;
+        --hamburger-active-color: black;
+        --hamburger-border-color: #717171;
+
+        --tags-border-color: #AAA;
+    }
+}
+
+[data-theme="dark"] {
     color-scheme: dark;
 
     --header-bg: #111010;
@@ -82,7 +110,6 @@ nav { line-height: normal; }
 
     --tags-border-color: #AAA;
 }
-}
 
 @supports (width: min(10px, 5vw)) {
     :root {
@@ -413,6 +440,44 @@ nav {
     --header-height: 0;
 }
 
+#settings {
+    margin-top: 5em;
+}
+#settings h3 {
+    font-size: inherit;
+}
+
+#color-theme-switcher {
+    display: flex;
+    justify-content: space-between;
+    padding: 0 2ex;
+    flex-flow: row wrap;
+}
+
+/* custom radio buttons for dark/light switch */
+#color-theme-switcher input {
+    -webkit-appearance: none;
+    -moz-appearance: none;
+    appearance: none;
+    display: inline-block;
+    box-sizing: content-box;
+    height: 1em;
+    width: 1em;
+    background-clip: content-box;
+    padding: 2px;
+    border: 2px solid transparent;
+    margin-bottom: -4px;
+    border-radius: 50%;
+}
+#color-theme-dark { background-color: #444; }
+#color-theme-light { background-color: #ccc; }
+#color-theme-system {
+    background-image: linear-gradient(60deg, #444, #444 50%, #CCC 50%, #CCC);
+}
+#color-theme-switcher input:checked {
+    border-color: var(--text-color);
+}
+
 .decl > div, .mod_doc {
     padding-left: 8px;
     padding-right: 8px;