about summary refs log tree commit diff
diff options
context:
space:
mode:
authorSerial <69764315+Serial-ATA@users.noreply.github.com>2022-04-24 16:10:01 -0400
committerSerial <69764315+Serial-ATA@users.noreply.github.com>2022-04-26 18:21:22 -0400
commitbdc896165928de3e04b02f3f5632094fe337ebbc (patch)
tree88deb59bdf754decec6891f98a786619b334cdbd
parent6aa3684431e85609eab1168098915afcb4e20d65 (diff)
downloadrust-bdc896165928de3e04b02f3f5632094fe337ebbc.tar.gz
rust-bdc896165928de3e04b02f3f5632094fe337ebbc.zip
Add version filtering option to the lint list
-rw-r--r--util/gh-pages/index.html164
1 files changed, 151 insertions, 13 deletions
diff --git a/util/gh-pages/index.html b/util/gh-pages/index.html
index 97c974003c6..286f3a34753 100644
--- a/util/gh-pages/index.html
+++ b/util/gh-pages/index.html
@@ -94,6 +94,20 @@ Otherwise, have a great day =^.^=
         @media (min-width: 992px) {
             .search-control {
                 margin-top: 0;
+                float: right;
+            }
+        }
+
+        @media (min-width: 400px) {
+            #upper-filters {
+                display: flex;
+            }
+        }
+
+        @media (max-width: 412px) {
+            #version-filter-selector {
+                right: 0;
+                left: auto;
             }
         }
 
@@ -244,7 +258,7 @@ Otherwise, have a great day =^.^=
             cursor: pointer;
         }
 
-        .theme-choice>li:hover {
+        .theme-choice > li:hover {
             background: var(--theme-hover);
         }
 
@@ -273,23 +287,40 @@ 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: 80%;
+        }
+
+        .version-filter-input {
+            height: 75%;
+        }
+
+        #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 +369,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 +422,36 @@ 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 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 version_filters">
+                                        <label>
+                                            <input type="checkbox" ng-model="version_filters[filter].enabled" />
+                                            {{filter}}
+                                        </label>
+                                        <input type="text" class="version-filter-input form-control filter-input" maxlength="6" placeholder="1.62.0" ng-model="version_filters[filter].version_str" ng-model-options="{debounce: 50}"/>
+                                    </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 +460,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">
@@ -601,6 +655,15 @@ Otherwise, have a great day =^.^=
             };
             $scope.themes = THEMES_DEFAULT;
 
+            const DEFAULT_VERSION_FILTERS = {
+                ">=": { enabled: false, version_str: "" },
+                "<=": { enabled: false, version_str: "" },
+                "==": { enabled: false, version_str: "" },
+            };
+            // Weird workaround to get a copy of the object
+            $scope.version_filters = JSON.parse(JSON.stringify(DEFAULT_VERSION_FILTERS));
+            $scope.version_regex = new RegExp('\\d\.\\d{2}\.\\d');
+
             $scope.selectTheme = function (theme) {
                 setTheme(theme, true);
             }
@@ -613,6 +676,7 @@ Otherwise, have a great day =^.^=
                     }
                 }
             };
+
             $scope.toggleGroups = function (value) {
                 const groups = $scope.groups;
                 for (const key in groups) {
@@ -621,9 +685,83 @@ Otherwise, have a great day =^.^=
                     }
                 }
             };
+
             $scope.selectedValuesCount = function (obj) {
                 return Object.values(obj).filter(x => x).length;
             }
+
+            $scope.clearVersionFilters = function () {
+                $scope.version_filters = JSON.parse(JSON.stringify(DEFAULT_VERSION_FILTERS));
+            }
+
+            $scope.versionSymbol = function() {
+                const version_filters = $scope.version_filters;
+                let filter = ">=";
+                for (const key in version_filters) {
+                    if (version_filters[key]) {
+                        filter = key;
+                    }
+                }
+
+                return filter;
+            }
+
+            $scope.byVersion = function(lint) {
+                function validate_version_str(ver) {
+                    return ver.length === 6 && $scope.version_regex.test(ver);
+                }
+
+                function cmp_version(ver1, ver2, filter) {
+                    // < 0: lint_version < version
+                    // 0: equal
+                    // > 0: lint_version > version
+                    let result = ver1.localeCompare(ver2, undefined, {
+                        numeric: true,
+                        sensitivity: "base"
+                    });
+
+                    // "==" gets the highest priority, since all filters are inclusive
+                    return (result === 0) || (filter === ">=" && result > 0) || (filter === "<=" && result < 0);
+                }
+
+                let filters = $scope.version_filters;
+
+                // Strip the "pre " prefix for pre 1.29.0 lints
+                let lint_version = lint.version.startsWith("pre ") ? lint.version.substring(4, lint.version.length) : lint.version;
+
+                for (const filter in filters) {
+                    let version_str = filters[filter].version_str;
+
+                    // Skip the work for version strings with invalid lengths or characters
+                    if (!filters[filter].enabled || !validate_version_str(version_str)) {
+                        continue;
+                    }
+
+                    let result = cmp_version(lint_version, version_str, filter);
+                    if (result && filter === "==") {
+                        return true;
+                    } else if (!result) {
+                        return false;
+                    }
+
+                    let cmp_filter;
+                    if (filter === ">=") {
+                        cmp_filter = "<=";
+                    } else {
+                        cmp_filter = ">=";
+                    }
+
+                    let cmp_version_str = filters[cmp_filter].version_str;
+                    if (!filters[cmp_filter].enabled || !validate_version_str(cmp_version_str)) {
+                        return true;
+                    }
+
+                    return cmp_version(lint_version, cmp_version_str, cmp_filter);
+                }
+
+                return true;
+            }
+
             $scope.byGroups = function (lint) {
                 return $scope.groups[lint.group];
             };
@@ -753,4 +891,4 @@ Otherwise, have a great day =^.^=
     setTheme(localStorage.getItem('clippy-lint-list-theme'), false);
     </script>
 </body>
-</html>
+</html>
\ No newline at end of file