Auto merge of #8752 - Serial-ATA:improve-filtering, r=xFrednet

Add version filtering option to the lint list

I'm no web dev, so I don't know if this is the best execution :smile:.

Here's how it looks:

![Desktop](https://user-images.githubusercontent.com/69764315/165403602-9e39fe0f-6a96-46cb-ba51-8b035e74cce4.gif)

And on mobile:

![Mobile](https://user-images.githubusercontent.com/69764315/165403908-fc4a0051-2ed4-48a3-b45b-b261f49ce259.png)

I've split this into two commits, in the second one I moved the JS into its own file to make it easier to work on. Is that alright? And if so, could the same thing be done to the css?

changelog: none
cc: #7958, `@repi`
r? `@xFrednet`

3 files changed, 442 insertions, 302 deletions

diff --git a/.github/deploy.sh b/.github/deploy.sh
index 34225a54029..5a59f94ec91 100644
--- a/.github/deploy.sh
+++ b/.github/deploy.sh
@@ -8,6 +8,7 @@ rm -rf out/master/ || exit 0
 echo "Making the docs for master"
 mkdir out/master/
 cp util/gh-pages/index.html out/master
+cp util/gh-pages/script.js out/master
 cp util/gh-pages/lints.json out/master
 
 if [[ -n $TAG_NAME ]]; then
diff --git a/util/gh-pages/index.html b/util/gh-pages/index.html
index 97c974003c6..1171da3f4e5 100644
--- a/util/gh-pages/index.html
+++ b/util/gh-pages/index.html
@@ -94,6 +94,29 @@ Otherwise, have a great day =^.^=
         @media (min-width: 992px) {
             .search-control {
                 margin-top: 0;
+                float: right;
+            }
+        }
+
+        @media (min-width: 405px) {
+            #upper-filters {
+                display: flex;
+            }
+        }
+
+        @media (max-width: 430px) {
+            /* Turn the version filter list to the left */
+            #version-filter-selector {
+                right: 0;
+                left: auto;
+            }
+        }
+
+        @media (max-width: 412px) {
+            #upper-filters,
+            .panel-body .search-control  {
+                padding-right: 8px;
+                padding-left: 8px;
             }
         }
 
@@ -244,7 +267,7 @@ Otherwise, have a great day =^.^=
             cursor: pointer;
         }
 
-        .theme-choice>li:hover {
+        .theme-choice > li:hover {
             background: var(--theme-hover);
         }
 
@@ -273,23 +296,44 @@ Otherwise, have a great day =^.^=
             border: 1px solid var(--theme-popup-border);
         }
 
-        #filter-label, #filter-clear {
+        #version-filter-selector .checkbox {
+            display: flex;
+        }
+
+        #version-filter {
+            min-width: available;
+        }
+
+        #version-filter li label {
+            padding-right: 0;
+            width: 35%;
+        }
+
+        .version-filter-input {
+            height: 60%;
+            width: 30%;
+            text-align: center;
+            border: none;
+            border-bottom: 1px solid #000000;
+        }
+
+        #filter-label, .filter-clear {
             background: var(--searchbar-bg);
             color: var(--searchbar-fg);
             border-color: var(--theme-popup-border);
             filter: brightness(95%);
         }
-        #filter-label:hover, #filter-clear:hover {
+        #filter-label:hover, .filter-clear:hover {
             filter: brightness(90%);
         }
-        #filter-input {
+        .filter-input {
             background: var(--searchbar-bg);
             color: var(--searchbar-fg);
             border-color: var(--theme-popup-border);
         }
 
-        #filter-input::-webkit-input-placeholder,
-        #filter-input::-moz-placeholder {
+        .filter-input::-webkit-input-placeholder,
+        .filter-input::-moz-placeholder {
             color: var(--searchbar-fg);
             opacity: 30%;
         }
@@ -338,7 +382,7 @@ Otherwise, have a great day =^.^=
 
             <div class="panel panel-default" ng-show="data">
                 <div class="panel-body row">
-                    <div class="col-12 col-md-4">
+                    <div id="upper-filters" class="col-12 col-md-4">
                         <div class="btn-group" filter-dropdown>
                             <button type="button" class="btn btn-default dropdown-toggle">
                                 Lint levels <span class="badge">{{selectedValuesCount(levels)}}</span> <span class="caret"></span>
@@ -391,13 +435,47 @@ Otherwise, have a great day =^.^=
                                 </li>
                             </ul>
                         </div>
+                        <div id="version-filter">
+                            <div class="btn-group" filter-dropdown>
+                                <button type="button" class="btn btn-default dropdown-toggle">
+                                    Version
+                                    <span id="version-filter-count" class="badge">
+                                        {{versionFilterCount(versionFilters)}}
+                                    </span>
+                                    <span class="caret"></span>
+                                </button>
+                                <ul id="version-filter-selector" class="dropdown-menu">
+                                    <li class="checkbox">
+                                        <label ng-click="clearVersionFilters()">
+                                            <input type="checkbox" class="invisible" />
+                                            Clear filters
+                                        </label>
+                                    </li>
+                                    <li role="separator" class="divider"></li>
+                                    <li class="checkbox" ng-repeat="(filter, vars) in versionFilters">
+                                        <label ng-attr-for="filter-{filter}">{{filter}}</label>
+                                        <span>1.</span>
+                                        <input type="number"
+                                                min="29"
+                                                ng-attr-id="filter-{filter}"
+                                                class="version-filter-input form-control filter-input"
+                                                maxlength="2"
+                                                ng-model="versionFilters[filter].minorVersion"
+                                                ng-model-options="{debounce: 50}"
+                                                ng-change="updateVersionFilters()" />
+                                        <span>.0</span>
+                                    </li>
+                                </ul>
+                            </div>
+                        </div>
+
                     </div>
-                    <div class="col-12 col-md-8 search-control">
+                    <div class="col-12 col-md-7 search-control">
                         <div class="input-group">
-                            <label class="input-group-addon" id="filter-label" for="filter-input">Filter:</label>
-                            <input type="text" class="form-control" placeholder="Keywords or search string" id="filter-input" ng-model="search" ng-model-options="{debounce: 50}"/>
+                            <label class="input-group-addon" id="filter-label" for="search-input">Filter:</label>
+                            <input type="text" class="form-control filter-input" placeholder="Keywords or search string" id="search-input" ng-model="search" ng-model-options="{debounce: 50}"/>
                             <span class="input-group-btn">
-                                <button id="filter-clear" class="btn" type="button" ng-click="search = ''">
+                                <button class="filter-clear btn" type="button" ng-click="search = ''">
                                     Clear
                                 </button>
                             </span>
@@ -406,7 +484,7 @@ Otherwise, have a great day =^.^=
                 </div>
             </div>
             <!-- The order of the filters should be from most likely to remove a lint to least likely to improve performance. -->
-            <article class="panel panel-default" id="{{lint.id}}" ng-repeat="lint in data | filter:bySearch | filter:byGroups | filter:byLevels">
+            <article class="panel panel-default" id="{{lint.id}}" ng-repeat="lint in data | filter:bySearch | filter:byGroups | filter:byLevels | filter:byVersion">
                 <header class="panel-heading" ng-click="open[lint.id] = !open[lint.id]">
                     <h2 class="panel-title">
                         <div class="panel-title-name">
@@ -462,295 +540,6 @@ Otherwise, have a great day =^.^=
     <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.5.0/highlight.min.js"></script>
     <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.5.0/languages/rust.min.js"></script>
     <script src="https://cdnjs.cloudflare.com/ajax/libs/angular.js/1.4.12/angular.min.js"></script>
-    <script>
-    (function () {
-        var md = window.markdownit({
-            html: true,
-            linkify: true,
-            typographer: true,
-            highlight: function (str, lang) {
-                if (lang && hljs.getLanguage(lang)) {
-                    try {
-                        return '<pre class="hljs"><code>' +
-                            hljs.highlight(lang, str, true).value +
-                            '</code></pre>';
-                    } catch (__) {}
-                }
-
-                return '<pre class="hljs"><code>' + md.utils.escapeHtml(str) + '</code></pre>';
-            }
-        });
-
-        function scrollToLint(lintId) {
-            var target = document.getElementById(lintId);
-            if (!target) {
-                return;
-            }
-            target.scrollIntoView();
-        }
-
-        function scrollToLintByURL($scope) {
-            var removeListener = $scope.$on('ngRepeatFinished', function(ngRepeatFinishedEvent) {
-                scrollToLint(window.location.hash.slice(1));
-                removeListener();
-            });
-        }
-
-        function selectGroup($scope, selectedGroup) {
-            var groups = $scope.groups;
-            for (var group in groups) {
-                if (groups.hasOwnProperty(group)) {
-                    if (group === selectedGroup) {
-                        groups[group] = true;
-                    } else {
-                        groups[group] = false;
-                    }
-                }
-            }
-        }
-
-        angular.module("clippy", [])
-        .filter('markdown', function ($sce) {
-            return function (text) {
-                return $sce.trustAsHtml(
-                    md.render(text || '')
-                    // Oh deer, what a hack :O
-                    .replace('<table', '<table class="table"')
-                );
-            };
-        })
-        .directive('themeDropdown', function ($document) {
-            return {
-                restrict: 'A',
-                link: function ($scope, $element, $attr) {
-                    $element.bind('click', function () {
-                        $element.toggleClass('open');
-                        $element.addClass('open-recent');
-                    });
-
-                    $document.bind('click', function () {
-                        if (!$element.hasClass('open-recent')) {
-                            $element.removeClass('open');
-                        }
-                        $element.removeClass('open-recent');
-                    })
-                }
-            }
-        })
-        .directive('filterDropdown', function ($document) {
-            return {
-                restrict: 'A',
-                link: function ($scope, $element, $attr) {
-                    $element.bind('click', function (event) {
-                        if (event.target.closest('button')) {
-                            $element.toggleClass('open');
-                        } else {
-                            $element.addClass('open');
-                        }
-                        $element.addClass('open-recent');
-                    });
-
-                    $document.bind('click', function () {
-                        if (!$element.hasClass('open-recent')) {
-                            $element.removeClass('open');
-                        }
-                        $element.removeClass('open-recent');
-                    })
-                }
-            }
-        })
-        .directive('onFinishRender', function ($timeout) {
-            return {
-                restrict: 'A',
-                link: function (scope, element, attr) {
-                    if (scope.$last === true) {
-                        $timeout(function () {
-                            scope.$emit(attr.onFinishRender);
-                        });
-                    }
-                }
-            };
-        })
-        .controller("lintList", function ($scope, $http, $timeout) {
-            // Level filter
-            var LEVEL_FILTERS_DEFAULT = {allow: true, warn: true, deny: true, none: true};
-            $scope.levels = LEVEL_FILTERS_DEFAULT;
-            $scope.byLevels = function (lint) {
-                return $scope.levels[lint.level];
-            };
-
-            var GROUPS_FILTER_DEFAULT = {
-                cargo: true,
-                complexity: true,
-                correctness: true,
-                deprecated: false,
-                nursery: true,
-                pedantic: true,
-                perf: true,
-                restriction: true,
-                style: true,
-                suspicious: true,
-            };
-            $scope.groups = GROUPS_FILTER_DEFAULT;
-            const THEMES_DEFAULT = {
-                light: "Light",
-                rust: "Rust",
-                coal: "Coal",
-                navy: "Navy",
-                ayu: "Ayu"
-            };
-            $scope.themes = THEMES_DEFAULT;
-
-            $scope.selectTheme = function (theme) {
-                setTheme(theme, true);
-            }
-
-            $scope.toggleLevels = function (value) {
-                const levels = $scope.levels;
-                for (const key in levels) {
-                    if (levels.hasOwnProperty(key)) {
-                        levels[key] = value;
-                    }
-                }
-            };
-            $scope.toggleGroups = function (value) {
-                const groups = $scope.groups;
-                for (const key in groups) {
-                    if (groups.hasOwnProperty(key)) {
-                        groups[key] = value;
-                    }
-                }
-            };
-            $scope.selectedValuesCount = function (obj) {
-                return Object.values(obj).filter(x => x).length;
-            }
-            $scope.byGroups = function (lint) {
-                return $scope.groups[lint.group];
-            };
-
-            $scope.bySearch = function (lint, index, array) {
-                let searchStr = $scope.search;
-                // It can be `null` I haven't missed this value
-                if (searchStr == null || searchStr.length < 3) {
-                    return true;
-                }
-                searchStr = searchStr.toLowerCase();
-
-                // Search by id
-                if (lint.id.indexOf(searchStr.replace("-", "_")) !== -1) {
-                    return true;
-                }
-
-                // Search the description
-                // The use of `for`-loops instead of `foreach` enables us to return early
-                let terms = searchStr.split(" ");
-                let docsLowerCase = lint.docs.toLowerCase();
-                for (index = 0; index < terms.length; index++) {
-                    // This is more likely and will therefor be checked first
-                    if (docsLowerCase.indexOf(terms[index]) !== -1) {
-                        continue;
-                    }
-
-                    if (lint.id.indexOf(terms[index]) !== -1) {
-                        continue;
-                    }
-
-                    return false;
-                }
-
-                return true;
-            }
-
-            // Get data
-            $scope.open = {};
-            $scope.loading = true;
-            // This will be used to jump into the source code of the version that this documentation is for.
-            $scope.docVersion = window.location.pathname.split('/')[2] || "master";
-
-            if (window.location.hash.length > 1) {
-                $scope.search = window.location.hash.slice(1);
-                $scope.open[window.location.hash.slice(1)] = true;
-                scrollToLintByURL($scope);
-            }
-
-            $http.get('./lints.json')
-            .success(function (data) {
-                $scope.data = data;
-                $scope.loading = false;
-
-                var selectedGroup = getQueryVariable("sel");
-                if (selectedGroup) {
-                    selectGroup($scope, selectedGroup.toLowerCase());
-                }
-
-                scrollToLintByURL($scope);
-
-                setTimeout(function () {
-                    var el = document.getElementById('filter-input');
-                    if (el) { el.focus() }
-                }, 0);
-            })
-            .error(function (data) {
-                $scope.error = data;
-                $scope.loading = false;
-            });
-
-            window.addEventListener('hashchange', function () {
-                // trigger re-render
-                $timeout(function () {
-                    $scope.levels = LEVEL_FILTERS_DEFAULT;
-                    $scope.search = window.location.hash.slice(1);
-                    $scope.open[window.location.hash.slice(1)] = true;
-
-                    scrollToLintByURL($scope);
-                });
-                return true;
-            }, false);
-        });
-    })();
-
-    function getQueryVariable(variable) {
-        var query = window.location.search.substring(1);
-        var vars = query.split('&');
-        for (var i = 0; i < vars.length; i++) {
-            var pair = vars[i].split('=');
-            if (decodeURIComponent(pair[0]) == variable) {
-                return decodeURIComponent(pair[1]);
-            }
-        }
-    }
-
-    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);
-    </script>
+    <script src="script.js"></script>
 </body>
 </html>
diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
new file mode 100644
index 00000000000..c3250afdea2
--- /dev/null
+++ b/util/gh-pages/script.js
@@ -0,0 +1,350 @@
+(function () {
+    var md = window.markdownit({
+        html: true,
+        linkify: true,
+        typographer: true,
+        highlight: function (str, lang) {
+            if (lang && hljs.getLanguage(lang)) {
+                try {
+                    return '<pre class="hljs"><code>' +
+                        hljs.highlight(lang, str, true).value +
+                        '</code></pre>';
+                } catch (__) {}
+            }
+
+            return '<pre class="hljs"><code>' + md.utils.escapeHtml(str) + '</code></pre>';
+        }
+    });
+
+    function scrollToLint(lintId) {
+        var target = document.getElementById(lintId);
+        if (!target) {
+            return;
+        }
+        target.scrollIntoView();
+    }
+
+    function scrollToLintByURL($scope) {
+        var removeListener = $scope.$on('ngRepeatFinished', function(ngRepeatFinishedEvent) {
+            scrollToLint(window.location.hash.slice(1));
+            removeListener();
+        });
+    }
+
+    function selectGroup($scope, selectedGroup) {
+        var groups = $scope.groups;
+        for (var group in groups) {
+            if (groups.hasOwnProperty(group)) {
+                if (group === selectedGroup) {
+                    groups[group] = true;
+                } else {
+                    groups[group] = false;
+                }
+            }
+        }
+    }
+
+    angular.module("clippy", [])
+        .filter('markdown', function ($sce) {
+            return function (text) {
+                return $sce.trustAsHtml(
+                    md.render(text || '')
+                        // Oh deer, what a hack :O
+                        .replace('<table', '<table class="table"')
+                );
+            };
+        })
+        .directive('themeDropdown', function ($document) {
+            return {
+                restrict: 'A',
+                link: function ($scope, $element, $attr) {
+                    $element.bind('click', function () {
+                        $element.toggleClass('open');
+                        $element.addClass('open-recent');
+                    });
+
+                    $document.bind('click', function () {
+                        if (!$element.hasClass('open-recent')) {
+                            $element.removeClass('open');
+                        }
+                        $element.removeClass('open-recent');
+                    })
+                }
+            }
+        })
+        .directive('filterDropdown', function ($document) {
+            return {
+                restrict: 'A',
+                link: function ($scope, $element, $attr) {
+                    $element.bind('click', function (event) {
+                        if (event.target.closest('button')) {
+                            $element.toggleClass('open');
+                        } else {
+                            $element.addClass('open');
+                        }
+                        $element.addClass('open-recent');
+                    });
+
+                    $document.bind('click', function () {
+                        if (!$element.hasClass('open-recent')) {
+                            $element.removeClass('open');
+                        }
+                        $element.removeClass('open-recent');
+                    })
+                }
+            }
+        })
+        .directive('onFinishRender', function ($timeout) {
+            return {
+                restrict: 'A',
+                link: function (scope, element, attr) {
+                    if (scope.$last === true) {
+                        $timeout(function () {
+                            scope.$emit(attr.onFinishRender);
+                        });
+                    }
+                }
+            };
+        })
+        .controller("lintList", function ($scope, $http, $timeout) {
+            // Level filter
+            var LEVEL_FILTERS_DEFAULT = {allow: true, warn: true, deny: true, none: true};
+            $scope.levels = LEVEL_FILTERS_DEFAULT;
+            $scope.byLevels = function (lint) {
+                return $scope.levels[lint.level];
+            };
+
+            var GROUPS_FILTER_DEFAULT = {
+                cargo: true,
+                complexity: true,
+                correctness: true,
+                deprecated: false,
+                nursery: true,
+                pedantic: true,
+                perf: true,
+                restriction: true,
+                style: true,
+                suspicious: true,
+            };
+            $scope.groups = GROUPS_FILTER_DEFAULT;
+            const THEMES_DEFAULT = {
+                light: "Light",
+                rust: "Rust",
+                coal: "Coal",
+                navy: "Navy",
+                ayu: "Ayu"
+            };
+            $scope.themes = THEMES_DEFAULT;
+
+            $scope.versionFilters = {
+                "≥": {enabled: false, minorVersion: null },
+                "≤": {enabled: false, minorVersion: null },
+                "=": {enabled: false, minorVersion: null },
+            };
+
+            $scope.selectTheme = function (theme) {
+                setTheme(theme, true);
+            }
+
+            $scope.toggleLevels = function (value) {
+                const levels = $scope.levels;
+                for (const key in levels) {
+                    if (levels.hasOwnProperty(key)) {
+                        levels[key] = value;
+                    }
+                }
+            };
+
+            $scope.toggleGroups = function (value) {
+                const groups = $scope.groups;
+                for (const key in groups) {
+                    if (groups.hasOwnProperty(key)) {
+                        groups[key] = value;
+                    }
+                }
+            };
+
+            $scope.selectedValuesCount = function (obj) {
+                return Object.values(obj).filter(x => x).length;
+            }
+
+            $scope.clearVersionFilters = function () {
+                for (let filter in $scope.versionFilters) {
+                    $scope.versionFilters[filter] = { enabled: false, minorVersion: null };
+                }
+            }
+
+            $scope.versionFilterCount = function(obj) {
+                return Object.values(obj).filter(x => x.enabled).length;
+            }
+
+            $scope.updateVersionFilters = function() {
+                for (const filter in $scope.versionFilters) {
+                    let minorVersion = $scope.versionFilters[filter].minorVersion;
+
+                    // 1.29.0 and greater
+                    if (minorVersion && minorVersion > 28) {
+                        $scope.versionFilters[filter].enabled = true;
+                        continue;
+                    }
+
+                    $scope.versionFilters[filter].enabled = false;
+                }
+            }
+
+            $scope.byVersion = function(lint) {
+                let filters = $scope.versionFilters;
+                for (const filter in filters) {
+                    if (filters[filter].enabled) {
+                        let minorVersion = filters[filter].minorVersion;
+
+                        // Strip the "pre " prefix for pre 1.29.0 lints
+                        let lintVersion = lint.version.startsWith("pre ") ? lint.version.substring(4, lint.version.length) : lint.version;
+                        let lintMinorVersion = lintVersion.substring(2, 4);
+
+                        switch (filter) {
+                            // "=" gets the highest priority, since all filters are inclusive
+                            case "=":
+                                return (lintMinorVersion == minorVersion);
+                            case "≥":
+                                if (lintMinorVersion < minorVersion) { return false; }
+                                break;
+                            case "≤":
+                                if (lintMinorVersion > minorVersion) { return false; }
+                                break;
+                            default:
+                                return true
+                        }
+                    }
+                }
+
+                return true;
+            }
+
+            $scope.byGroups = function (lint) {
+                return $scope.groups[lint.group];
+            };
+
+            $scope.bySearch = function (lint, index, array) {
+                let searchStr = $scope.search;
+                // It can be `null` I haven't missed this value
+                if (searchStr == null || searchStr.length < 3) {
+                    return true;
+                }
+                searchStr = searchStr.toLowerCase();
+
+                // Search by id
+                if (lint.id.indexOf(searchStr.replace("-", "_")) !== -1) {
+                    return true;
+                }
+
+                // Search the description
+                // The use of `for`-loops instead of `foreach` enables us to return early
+                let terms = searchStr.split(" ");
+                let docsLowerCase = lint.docs.toLowerCase();
+                for (index = 0; index < terms.length; index++) {
+                    // This is more likely and will therefor be checked first
+                    if (docsLowerCase.indexOf(terms[index]) !== -1) {
+                        continue;
+                    }
+
+                    if (lint.id.indexOf(terms[index]) !== -1) {
+                        continue;
+                    }
+
+                    return false;
+                }
+
+                return true;
+            }
+
+            // Get data
+            $scope.open = {};
+            $scope.loading = true;
+            // This will be used to jump into the source code of the version that this documentation is for.
+            $scope.docVersion = window.location.pathname.split('/')[2] || "master";
+
+            if (window.location.hash.length > 1) {
+                $scope.search = window.location.hash.slice(1);
+                $scope.open[window.location.hash.slice(1)] = true;
+                scrollToLintByURL($scope);
+            }
+
+            $http.get('./lints.json')
+                .success(function (data) {
+                    $scope.data = data;
+                    $scope.loading = false;
+
+                    var selectedGroup = getQueryVariable("sel");
+                    if (selectedGroup) {
+                        selectGroup($scope, selectedGroup.toLowerCase());
+                    }
+
+                    scrollToLintByURL($scope);
+
+                    setTimeout(function () {
+                        var el = document.getElementById('filter-input');
+                        if (el) { el.focus() }
+                    }, 0);
+                })
+                .error(function (data) {
+                    $scope.error = data;
+                    $scope.loading = false;
+                });
+
+            window.addEventListener('hashchange', function () {
+                // trigger re-render
+                $timeout(function () {
+                    $scope.levels = LEVEL_FILTERS_DEFAULT;
+                    $scope.search = window.location.hash.slice(1);
+                    $scope.open[window.location.hash.slice(1)] = true;
+
+                    scrollToLintByURL($scope);
+                });
+                return true;
+            }, false);
+        });
+})();
+
+function getQueryVariable(variable) {
+    var query = window.location.search.substring(1);
+    var vars = query.split('&');
+    for (var i = 0; i < vars.length; i++) {
+        var pair = vars[i].split('=');
+        if (decodeURIComponent(pair[0]) == variable) {
+            return decodeURIComponent(pair[1]);
+        }
+    }
+}
+
+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);