Auto merge of #13178 - GuillaumeGomez:clippy-lints-page-improvement, r=Alexendoo

Add possibility to focus on search input using keyboard

This PR adds the possibility to focus on the search input with `S` or `/` like in rustdoc and `mdbook` and `docs.rs` (unification++). Pressing escape will blur it.

r? `@Alexendoo`

changelog: Add possibility to focus on search input using keyboard

Author: bors

util/gh-pages/index.html

@@ -541,7 +541,7 @@ <h1>Clippy Lints</h1>
                     <div class="col-12 col-md-5 search-control">
                         <div class="input-group">
                             <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"
+                            <input type="text" class="form-control filter-input" placeholder="Keywords or search string (`S` or `/` to focus)" id="search-input"
                                 ng-model="search" ng-blur="updatePath()" ng-keyup="$event.keyCode == 13 && updatePath()"
                                 ng-model-options="{debounce: 50}" />
                             <span class="input-group-btn">

util/gh-pages/script.js

@@ -575,6 +575,32 @@ function setTheme(theme, store) {
     }
 }
 
+function handleShortcut(ev) {
+    if (ev.ctrlKey || ev.altKey || ev.metaKey) {
+        return;
+    }
+
+    if (document.activeElement.tagName === "INPUT") {
+        if (ev.key === "Escape") {
+            document.activeElement.blur();
+        }
+    } else {
+        switch (ev.key) {
+            case "s":
+            case "S":
+            case "/":
+                ev.preventDefault(); // To prevent the key to be put into the input.
+                document.getElementById("search-input").focus();
+                break;
+            default:
+                break;
+        }
+    }
+}
+
+document.addEventListener("keypress", handleShortcut);
+document.addEventListener("keydown", handleShortcut);
+
 // loading the theme after the initial load
 const prefersDark = window.matchMedia("(prefers-color-scheme: dark)");
 const theme = localStorage.getItem('clippy-lint-list-theme');