Search bar navigation

CHANGES.md

@@ -8,6 +8,8 @@
 - Separate compilation of interface and implementation files, using a new
   `compile-src` command (@panglesd, #1067).
 - Add clock emoji before `@since` tag (@yawaramin, #1089)
+- 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/html_page.ml

@@ -31,7 +31,7 @@ let html_of_toc toc =
 
 let html_of_search () =
   let search_bar =
-    Html.(input ~a:[ a_class [ "search-bar" ]; a_placeholder "🔎 Search..." ] ())
+    Html.(input ~a:[ a_class [ "search-bar" ]; a_placeholder "🔎 Type '/' to search..." ] ())
   in
   let snake = Html.(div ~a:[ a_class [ "search-snake" ] ] []) in
   let search_result = Html.div ~a:[ Html.a_class [ "search-result" ] ] [] in

src/html_support_files/odoc.css

@@ -1034,7 +1034,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,87 @@ 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());
+  if (results.length === 0) return;
+  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 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 (  is_searching()
+            && 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);