diff options
| -rw-r--r-- | util/gh-pages/index_template.html | 4 | ||||
| -rw-r--r-- | util/gh-pages/style.css | 17 | ||||
| -rw-r--r-- | util/gh-pages/theme.js | 4 |
3 files changed, 22 insertions, 3 deletions
diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index f95fe76d996..deb0ef0b499 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -52,12 +52,12 @@ Otherwise, have a great day =^.^= <noscript> {# #} <div class="alert alert-danger" role="alert"> {# #} - Sorry, this site only works with JavaScript! :( {# #} + Lints search and filtering only works with JS enabled. :( {# #} </div> {# #} </noscript> {# #} <div> {# #} - <div class="panel panel-default"> {# #} + <div class="panel panel-default" id="menu-filters"> {# #} <div class="panel-body row"> {# #} <div id="upper-filters" class="col-12 col-md-5"> {# #} <div class="btn-group" id="lint-levels" tabindex="-1"> {# #} diff --git a/util/gh-pages/style.css b/util/gh-pages/style.css index d207996ab2f..896f2fdac76 100644 --- a/util/gh-pages/style.css +++ b/util/gh-pages/style.css @@ -204,7 +204,7 @@ details[open] { } /* Expanding the mdBook theme*/ -.light { +.light, body:not([class]) { --inline-code-bg: #f6f7f6; } .rust { @@ -220,6 +220,21 @@ details[open] { --inline-code-bg: #191f26; } +@media (prefers-color-scheme: dark) { + body:not([class]) { + /* + In case JS is disabled and the user's system is in dark mode, we take "coal" as default + dark theme. + */ + --inline-code-bg: #1d1f21; + } +} + +html:not(.js) #settings-dropdown, +html:not(.js)#menu-filters { + display: none; +} + #settings-dropdown { position: absolute; margin: 0.7em; diff --git a/util/gh-pages/theme.js b/util/gh-pages/theme.js index bc296955ddf..90f57d4469d 100644 --- a/util/gh-pages/theme.js +++ b/util/gh-pages/theme.js @@ -45,6 +45,10 @@ function setTheme(theme, store) { } (function() { + // This file is loaded first. If so, we add the `js` class on the `<html>` + // element. + document.documentElement.classList.add("js"); + // loading the theme after the initial load const prefersDark = window.matchMedia("(prefers-color-scheme: dark)"); const theme = loadValue("theme"); |