diff --git a/util/gh-pages/index.html b/util/gh-pages/index.html index 1852fb6640ec..39448eec2ef5 100644 --- a/util/gh-pages/index.html +++ b/util/gh-pages/index.html @@ -8,6 +8,13 @@ + + + + + + + + +
🖌
+ +
-
+

Lint levels

@@ -79,7 +209,7 @@

ALL the Clippy Lints

- @@ -320,6 +450,60 @@

} } } + + function setupListeners() { + let themeIcon = document.getElementById("theme-icon"); + let themeMenu = document.getElementById("theme-menu"); + themeIcon.addEventListener("click", function(e) { + if (themeMenu.style.display == "none") { + themeMenu.style.display = "block"; + } else { + themeMenu.style.display = "none"; + } + }); + + let children = themeMenu.children; + for (let index = 0; index < children.length; index++) { + let child = children[index]; + child.addEventListener("click", function(e) { + setTheme(child.id, true); + }); + } + } + + setupListeners(); + + function setTheme(theme, store) { + let enableHighlight = false; + let enableNight = false; + let enableAyu = false; + + if (theme == "ayu") { + enableAyu = true; + } else if (theme == "coal" || theme == "navy") { + enableNight = true; + } else if (theme == "rust") { + enableHighlight = true; + } else { + enableHighlight = true; + // this makes sure that an unknown theme request gets set to a known one + theme = "light"; + } + document.getElementsByTagName("body")[0].className = theme; + + document.getElementById("styleHighlight").disabled = !enableHighlight; + document.getElementById("styleNight").disabled = !enableNight; + document.getElementById("styleAyu").disabled = !enableAyu; + + if (store) { + try { + localStorage.setItem('clippy-lint-list-theme', theme); + } catch (e) { } + } + } + + // loading the theme after the initial load + setTheme(localStorage.getItem('clippy-lint-list-theme'), false);