diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index f21c609..ae4037e 100644 --- a/DocGen4/Output.lean +++ b/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), diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index d02bf99..e2ae134 100644 --- a/DocGen4/Output/Base.lean +++ b/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" @@ -155,7 +156,7 @@ are used in documentation generation, notably JS and CSS ones. def importedByJs : String := include_str "../../static/importedBy.js" def findJs : String := include_str "../../static/find/find.js" def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js" - + def alectryonCss : String := include_str "../../static/alectryon/alectryon.css" def alectryonJs : String := include_str "../../static/alectryon/alectryon.js" def docUtilsCss : String := include_str "../../static/alectryon/docutils_basic.css" diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 4280864..37b0bb6 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -62,6 +62,7 @@ def navbar : BaseHtmlM Html := do [← baseHtmlHeadDeclarations] + @@ -82,6 +83,18 @@ def navbar : BaseHtmlM Html := do -/

Library

{← moduleList} +
+ -- `input` is a void tag, but can be self-closed to make parsing easier. +

Color scheme

+
+ + + +
+
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 86d2be0..ad8e570 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/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", diff --git a/lakefile.lean b/lakefile.lean index 267bd15..7edfa3e 100644 --- a/lakefile.lean +++ b/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", diff --git a/static/color-scheme.js b/static/color-scheme.js new file mode 100644 index 0000000..4a1b6da --- /dev/null +++ b/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()); + }) +}); diff --git a/static/style.css b/static/style.css index cbed584..130d1c4 100644 --- a/static/style.css +++ b/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,10 +53,10 @@ 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 { - color-scheme: dark; - --header-bg: #111010; --body-bg: #171717; --code-bg: #363333; @@ -84,6 +83,34 @@ nav { line-height: normal; } } } +[data-theme="dark"] { + color-scheme: dark; + + --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; +} + @supports (width: min(10px, 5vw)) { :root { --content-width: clamp(20em, 55vw, 60em); @@ -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;