mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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

Browse Source 
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`
This commit is contained in:
bors 2024-11-02 13:49:04 +00:00
commit 52b8324503
3 changed files with 22 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
util/gh-pages/index_template.html
View File

@ -52,12 +52,12 @@ Otherwise, have a great day =^.^=
<noscript> {# #} <noscript> {# #}
<div class="alert alert-danger" role="alert"> {# #} <div class="alert alert-danger" role="alert"> {# #}
Sorry, this site only works with JavaScript! :( {# #} Lints search and filtering only works with JS enabled. :( {# #}
</div> {# #} </div> {# #}
</noscript> {# #} </noscript> {# #}
<div> {# #} <div> {# #}
<div class="panel panel-default"> {# #} <div class="panel panel-default" id="menu-filters"> {# #}
<div class="panel-body row"> {# #} <div class="panel-body row"> {# #}
<div id="upper-filters" class="col-12 col-md-5"> {# #} <div id="upper-filters" class="col-12 col-md-5"> {# #}
<div class="btn-group" id="lint-levels" tabindex="-1"> {# #} <div class="btn-group" id="lint-levels" tabindex="-1"> {# #}

17
util/gh-pages/style.css
View File

@ -204,7 +204,7 @@ details[open] {
} }
/* Expanding the mdBook theme*/ /* Expanding the mdBook theme*/
.light { .light, body:not([class]) {
--inline-code-bg: #f6f7f6; --inline-code-bg: #f6f7f6;
} }
.rust { .rust {
@ -220,6 +220,21 @@ details[open] {
--inline-code-bg: #191f26; --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 { #settings-dropdown {
position: absolute; position: absolute;
margin: 0.7em; margin: 0.7em;

4
util/gh-pages/theme.js
View File

@ -45,6 +45,10 @@ function setTheme(theme, store) {
} }
(function() { (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 // loading the theme after the initial load
const prefersDark = window.matchMedia("(prefers-color-scheme: dark)"); const prefersDark = window.matchMedia("(prefers-color-scheme: dark)");
const theme = loadValue("theme"); const theme = loadValue("theme");