about summary refs log tree commit diff
diff options
context:
space:
mode:
authorbors <bors@rust-lang.org>2024-11-02 13:49:04 +0000
committerbors <bors@rust-lang.org>2024-11-02 13:49:04 +0000
commit52b8324503d670646bc54a976bbc6baa9ddde08e (patch)
tree4ee165b164692ff9ae2a93ec786105ce9913f1bf
parent5c6fe68c006b83eeef0f7f0213cf04c7865f7585 (diff)
parentac764df8ab342d5d58ec0a51d900949db68f70ad (diff)
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`
-rw-r--r--util/gh-pages/index_template.html4
-rw-r--r--util/gh-pages/style.css17
-rw-r--r--util/gh-pages/theme.js4
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");