Skip to content

Commit 52b8324

Browse files
committed
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`
2 parents 5c6fe68 + ac764df commit 52b8324

3 files changed

Lines changed: 22 additions & 3 deletions

File tree

‎util/gh-pages/index_template.html‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,12 +52,12 @@ <h1>Clippy Lints</h1> {# #}
5252

5353
<noscript> {# #}
5454
<divclass="alert alert-danger" role="alert"> {# #}
55-
Sorry, this site only works with JavaScript! :( {# #}
55+
Lints search and filtering only works with JS enabled. :( {# #}
5656
</div> {# #}
5757
</noscript> {# #}
5858

5959
<div> {# #}
60-
<divclass="panel panel-default"> {# #}
60+
<divclass="panel panel-default"id="menu-filters"> {# #}
6161
<divclass="panel-body row"> {# #}
6262
<divid="upper-filters" class="col-12 col-md-5"> {# #}
6363
<divclass="btn-group" id="lint-levels" tabindex="-1"> {# #}

‎util/gh-pages/style.css‎

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -204,7 +204,7 @@ details[open] {
204204
}
205205

206206
/* Expanding the mdBook theme*/
207-
.light {
207+
.light,body:not([class]) {
208208
--inline-code-bg:#f6f7f6;
209209
}
210210
.rust {
@@ -220,6 +220,21 @@ details[open] {
220220
--inline-code-bg:#191f26;
221221
}
222222

223+
@media (prefers-color-scheme: dark) {
224+
body:not([class]) {
225+
/*
226+
In case JS is disabled and the user's system is in dark mode, we take "coal" as default
227+
dark theme.
228+
*/
229+
--inline-code-bg:#1d1f21;
230+
}
231+
}
232+
233+
html:not(.js) #settings-dropdown,
234+
html:not(.js)#menu-filters {
235+
display: none;
236+
}
237+
223238
#settings-dropdown {
224239
position: absolute;
225240
margin:0.7em;

‎util/gh-pages/theme.js‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,10 @@ function setTheme(theme, store) {
4545
}
4646

4747
(function(){
48+
// This file is loaded first. If so, we add the `js` class on the `<html>`
49+
// element.
50+
document.documentElement.classList.add("js");
51+
4852
// loading the theme after the initial load
4953
constprefersDark=window.matchMedia("(prefers-color-scheme: dark)");
5054
consttheme=loadValue("theme");

0 commit comments

Comments
 (0)