Merge 2d0a5ed into ff4c335

CHANGES.md

@@ -7,6 +7,8 @@
   (@panglesd, #976)
 - Separate compilation of interface and implementation files, using a new
   `compile-src` command (@panglesd, #1067).
+- Navigation for the search bar : use '/' to enter search, up and down arrows to
+  select a result, and enter to follow the selected link. (@EmileTrotignon, #1088)
 
 ### Changed
 

src/html_support_files/odoc.css

@@ -1028,7 +1028,7 @@ td.def-doc *:first-child {
   white-space: nowrap;
 }
 
-.odoc-search .search-entry:focus-visible {
+.odoc-search .search-result .search-entry:focus-visible {
   box-shadow: none;
   background-color: var(--target-background);
 }

src/html_support_files/odoc_search.js

@@ -64,3 +64,90 @@ document.querySelector(".search-bar").addEventListener("input", (ev) => {
   wait();
   worker.postMessage(ev.target.value);
 });
+
+
+/** Navigation */
+
+let search_result_elt = document.querySelector(".search-result")
+
+function search_results() {
+  return search_result_elt.children;
+}
+
+function enter_search() {
+  document.querySelector(".search-bar").focus();
+}
+
+function escape_search() {
+  document.activeElement.blur()
+}
+
+function focus_previous_result() {
+  let results = Array.from(search_results());
+  let current_focus = results.findIndex((elt) => (document.activeElement === elt));
+  if (current_focus === -1)
+    return;
+  else if (current_focus === 0)
+    enter_search();
+  else
+    results[current_focus - 1].focus();
+}
+
+function focus_next_result() {
+  let results = Array.from(search_results());
+  let current_focus = results.findIndex((elt) => (document.activeElement === elt));
+  if (current_focus === -1)
+    results[0].focus();
+  else if (current_focus + 1 === results.length)
+    return;
+  else
+    results[current_focus + 1].focus();
+}
+
+function enter_focus() {
+  if (n_focus === null) return;
+  let elt = current_result();
+  elt.click();
+}
+
+function is_searching() {
+  return (document.querySelectorAll(".odoc-search:focus-within").length > 0);
+}
+
+function is_typing() {
+  return (document.activeElement === document.querySelector(".search-bar"));
+}
+
+function handle_key_down(event) {
+  if (is_searching()) {
+    if (event.key === "ArrowUp") {
+      event.preventDefault();
+      focus_previous_result();
+    }
+    if (event.key === "ArrowDown") {
+      event.preventDefault();
+      focus_next_result();
+    }
+    if (event.key === "Escape") {
+      event.preventDefault();
+      escape_search();
+    }
+  }
+  if (!(is_typing())) {
+    let ascii = event.key.charCodeAt(0);
+    if (event.key === "/") {
+      event.preventDefault();
+      enter_search();
+    }
+    else if ( event.key.length === 1
+            && (ascii >= 65 && ascii <= 90) // lowercase letter
+            || (ascii >= 97 && ascii <= 122) // uppercase letter
+            || (ascii >= 48 && ascii <= 57) // numbers
+            || (ascii >= 32 && ascii <= 46) // ` ` to `.`
+            || (ascii >= 58 && ascii <= 64) // `:` to `@`
+            )
+      // We do not prevent default because we want the char to be added to the input
+      enter_search ();
+  }
+}
+document.addEventListener("keydown", handle_key_down);