diff --git a/util/gh-pages/index.html b/util/gh-pages/index.html
index 1b4677a3c0e..99e211654d1 100644
--- a/util/gh-pages/index.html
+++ b/util/gh-pages/index.html
@@ -501,9 +501,11 @@ Otherwise, have a great day =^.^=
-
+
-
diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index 868b63a27df..fd32225dabc 100644
--- a/util/gh-pages/script.js
+++ b/util/gh-pages/script.js
@@ -106,7 +106,7 @@
}
};
})
- .controller("lintList", function ($scope, $http, $location) {
+ .controller("lintList", function ($scope, $http, $location, $timeout) {
// Level filter
var LEVEL_FILTERS_DEFAULT = {allow: true, warn: true, deny: true, none: true};
$scope.levels = { ...LEVEL_FILTERS_DEFAULT };
@@ -265,12 +265,6 @@
}
}, true);
- $scope.$watch('search', function (newVal, oldVal) {
- if (newVal !== oldVal) {
- $location.path(newVal);
- }
- });
-
// Watch for changes in the URL path and update the search and lint display
$scope.$watch(function () {
return $location.path();
@@ -283,12 +277,33 @@
}
});
+ let debounceTimeout;
+ $scope.$watch('search', function (newVal, oldVal) {
+ if (newVal !== oldVal) {
+ if (debounceTimeout) {
+ $timeout.cancel(debounceTimeout);
+ }
+
+ debounceTimeout = $timeout(function () {
+ $location.path(newVal);
+ }, 1000);
+ }
+ });
+
$scope.$watch(function () {
return $location.search();
}, function (newParameters) {
loadFromURLParameters();
});
+ $scope.updatePath = function () {
+ if (debounceTimeout) {
+ $timeout.cancel(debounceTimeout);
+ }
+
+ $location.path($scope.search);
+ }
+
$scope.selectTheme = function (theme) {
setTheme(theme, true);
}