Auto merge of #13585 - GuillaumeGomez:no-js, r=Alexendoo

Improve display of clippy lints page when JS is disabled There is no point in displaying the settings menu and the filters if JS is disabled. So in this case, this PR simply hides it: ![image](https://github.com/user-attachments/assets/e96039a9-e698-49b7-bf2b-70e78442b305) For the theme handling though, I need to send a fix to mdBook first. But once done, it'll look as expected (dark if system is in dark mode). changelog: Improve clippy lints page display when JS is disabled. r? `@Alexendoo`
rust-lang · Nov 2, 2024 · 52b8324 · 52b8324
2 parents 5c6fe68 + ac764df
commit 52b8324
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 3 deletions.
diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html
@@ -52,12 +52,12 @@ <h1>Clippy Lints</h1> {# #}
 
         <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
@@ -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
@@ -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");