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 b45481f..6c4769c 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -155,6 +155,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" @@ -162,7 +163,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 75975b6..e2ab585 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} + diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 2667f89..329b778 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/DocGen4/Process/Hierarchy.lean @@ -92,6 +92,7 @@ partial def fromArrayExt (names : Array NameExt) : Hierarchy := def baseDirBlackList : HashSet String := HashSet.fromArray #[ "404.html", + "color-scheme.js", "declaration-data.js", "declarations", "find", diff --git a/lake-manifest.json b/lake-manifest.json index 2701e8e..dfdebc6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -7,10 +7,16 @@ "rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8", "name": "CMark", "inputRev?": "main"}}, + {"git": + {"url": "https://github.com/EdAyers/ProofWidgets4", + "subDir?": null, + "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8", + "name": "proofwidgets", + "inputRev?": "v0.0.11"}}, {"git": {"url": "https://github.com/leanprover/lake", "subDir?": null, - "rev": "0d4da61cbfe65f19ac7070c2c9f62f36db529c4c", + "rev": "6601a21f624e445f51200e563cf9c549bdebe46c", "name": "lake", "inputRev?": "master"}}, {"git": @@ -22,7 +28,7 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "47535ddd6cff5cf523b8914a5269639641b9bb54", + "rev": "e6dcb5445cacb4f329ab8faa078f746368bc5d3b", "name": "mathlib", "inputRev?": "master"}}, {"git": @@ -52,12 +58,12 @@ {"git": {"url": "https://github.com/leanprover/std4.git", "subDir?": null, - "rev": "176b4657e21ea6f5a1517c625ee97e89acad0126", + "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936", "name": "std4", "inputRev?": "main"}}, {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6", + "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936", "name": "std", "inputRev?": "main"}}]} diff --git a/lakefile.lean b/lakefile.lean index fa08094..2e17834 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -103,6 +103,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/lean-toolchain b/lean-toolchain index 02773ff..fae03ab 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-05-31 +leanprover/lean4:nightly-2023-06-10 diff --git a/static/color-scheme.js b/static/color-scheme.js new file mode 100644 index 0000000..5b061ee --- /dev/null +++ b/static/color-scheme.js @@ -0,0 +1,33 @@ +function getTheme() { + return localStorage.getItem("theme") || "system"; +} + +function setTheme(themeName) { + localStorage.setItem('theme', themeName); + if (themeName == "system") { + themeName = parent.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 + for (const win of [window, parent]) { + win.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. + parent.matchMedia('(prefers-color-scheme: dark)').addEventListener('change', event => { + setTheme(getTheme()); + }) +}); + +// un-hide the colorscheme picker +document.querySelector("#settings").removeAttribute('hidden'); \ No newline at end of file diff --git a/static/style.css b/static/style.css index 8135090..27179a6 100644 --- a/static/style.css +++ b/static/style.css @@ -6,7 +6,14 @@ body { font-family: 'Open Sans', sans-serif; + color: var(--text-color); + background: var(--body-bg); } + +a { + color: var(--link-color); +} + h1, h2, h3, h4, h5, h6 { font-family: 'Merriweather', serif; } @@ -16,10 +23,128 @@ nav { line-height: normal; } :root { --header-height: 3em; + --fragment-offset: calc(var(--header-height) + 1em); + --content-width: 55vw; + --header-bg: #f8f8f8; + --body-bg: white; + --code-bg: #f3f3f3; + --text-color: black; + --link-color: hsl(210, 100%, 30%); + + --implicit-arg-text-color: var(--text-color); + + --def-color: #92dce5; + --def-color-hsl-angle: 187; + --theorem-color: #8fe388; + --theorem-color-hsl-angle: 115; + --axiom-and-constant-color: #f44708; + --axiom-and-constant-color-hsl-angle: 16; + --structure-and-inductive-color: #f0a202; + --structure-and-inductive-color-hsl-angle: 40; + --starting-percentage: 100; + + --hamburger-bg-color: #eee; + --hamburger-active-color: white; + --hamburger-border-color: #ccc; + + --tags-border-color: #555; + --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="light"] { + color-scheme: light; + + --header-height: 3em; + --fragment-offset: calc(var(--header-height) + 1em); + --content-width: 55vw; + + --header-bg: #f8f8f8; + --body-bg: white; + --code-bg: #f3f3f3; + --text-color: black; + --link-color: hsl(210, 100%, 30%); + + --implicit-arg-text-color: var(--text-color); + + --def-color: #92dce5; + --def-color-hsl-angle: 187; + --theorem-color: #8fe388; + --theorem-color-hsl-angle: 115; + --axiom-and-constant-color: #f44708; + --axiom-and-constant-color-hsl-angle: 16; + --structure-and-inductive-color: #f0a202; + --structure-and-inductive-color-hsl-angle: 40; + --starting-percentage: 100; + + --hamburger-bg-color: #eee; + --hamburger-active-color: white; + --hamburger-border-color: #ccc; + + --tags-border-color: #555; + + --fragment-offset: calc(var(--header-height) + 1em); + --content-width: 55vw; +} + +[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); @@ -94,13 +219,13 @@ header { label[for="nav_toggle"] { display: inline-block; margin-right: 1em; - border: 1px solid #ccc; + border: 1px solid var(--hamburger-border-color); padding: 0.5ex 1ex; cursor: pointer; - background: #eee; + background: var(--hamburger-bg-color); } #nav_toggle:checked ~ * label[for="nav_toggle"] { - background: white; + background: var(--hamburger-active-color); } body header h1 { @@ -199,8 +324,8 @@ header header_filename { } #autocomplete_results .selected .result_link a { - background: white; - border-color: #f0a202; + background: var(--body-bg); + border-color: var(--structure-and-inductive-color); } @@ -349,6 +474,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; @@ -413,23 +576,23 @@ main h2, main h3, main h4, main h5, main h6 { } .def, .instance { - border-left: 10px solid #92dce5; - border-top: 2px solid #92dce5; + border-left: 10px solid var(--text-color); + border-top: 2px solid var(--text-color); } .theorem { - border-left: 10px solid #8fe388; - border-top: 2px solid #8fe388; + border-left: 10px solid var(--theorem-color); + border-top: 2px solid var(--theorem-color); } .axiom, .opaque { - border-left: 10px solid #f44708; - border-top: 2px solid #f44708; + border-left: 10px solid var(--axiom-and-constant-color); + border-top: 2px solid var(--axiom-and-constant-color); } .structure, .inductive, .class { - border-left: 10px solid #f0a202; - border-top: 2px solid #f0a202; + border-left: 10px solid var(--structure-and-inductive-color); + border-top: 2px solid var(--structure-and-inductive-color); } .fn { @@ -454,23 +617,23 @@ main h2, main h3, main h4, main h5, main h6 { } .def .fn:hover, .instance .fn:hover { - background-color: hsla(187, 61%, calc(100% - 5%*var(--fn))); - box-shadow: 0 0 0 1px hsla(187, 61%, calc(100% - 5%*(var(--fn) + 1))); + background-color: hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1))); border-radius: 5px; } .theorem .fn:hover { - background-color: hsla(115, 62%, calc(100% - 5%*var(--fn))); - box-shadow: 0 0 0 1px hsla(115, 62%, calc(100% - 5%*(var(--fn) + 1))); + background-color: hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1))); border-radius: 5px; } .axiom .fn:hover, .opaque .fn:hover { - background-color: hsla(16, 94%, calc(100% - 5%*var(--fn))); - box-shadow: 0 0 0 1px hsla(16, 94%, calc(100% - 5%*(var(--fn) + 1))); + background-color: hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1))); border-radius: 5px; } .structure .fn:hover, .inductive .fn:hover, .class .fn:hover { - background-color: hsla(40, 98%, calc(100% - 5%*var(--fn))); - box-shadow: 0 0 0 1px hsla(40, 98%, calc(100% - 5%*(var(--fn) + 1))); + background-color: hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1))); border-radius: 5px; } @@ -479,7 +642,7 @@ main h2, main h3, main h4, main h5, main h6 { } .implicits, .impl_arg { - color: black; + color: var(--text-color); white-space: normal; } @@ -515,7 +678,7 @@ pre { white-space: break-spaces; } -code, pre { background: #f3f3f3; } +code, pre { background: var(--code-bg); } code, pre { border-radius: 5px; } code { padding: 1px 3px; } pre { padding: 1ex; } @@ -539,11 +702,13 @@ pre code { padding: 0 0; } .inductive_ctor_doc { text-indent: 2ex; padding-top: 1ex; + font-family: 'Open Sans', sans-serif; } .structure_field_doc { text-indent: 0; padding-top: 1ex; + font-family: 'Open Sans', sans-serif; } .structure_ext_fields { @@ -572,7 +737,7 @@ pre code { padding: 0 0; } /** Don't show underline on types, to prevent the ≤ vs < confusion. **/ a:link, a:visited, a:active { - color:hsl(210, 100%, 30%); + color:var(--link-color); text-decoration: none; } @@ -608,7 +773,7 @@ a:hover { } .docfile h2 a { - color: black; + color: var(--text-color); } .tags { @@ -621,7 +786,7 @@ a:hover { } .tags li { - border: 1px solid #555; + border: 1px solid var(--tags-border-color); border-radius: 4px; list-style-type: none; padding: 1px 3px; @@ -637,4 +802,4 @@ a:hover { padding-top: 2em; margin-top: 2em; margin-bottom: 2em; -} +} \ No newline at end of file