diff --git a/CHANGES.md b/CHANGES.md index b567b5957b..1db0924002 100644 --- a/CHANGES.md +++ b/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 diff --git a/src/html/html_page.ml b/src/html/html_page.ml index 140f20113e..29e6681871 100644 --- a/src/html/html_page.ml +++ b/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 diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index 4fa970c97a..93dc1efd2c 100644 --- a/src/html_support_files/odoc.css +++ b/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); } diff --git a/src/html_support_files/odoc_search.js b/src/html_support_files/odoc_search.js index 0dc659d27d..79b86bd142 100644 --- a/src/html_support_files/odoc_search.js +++ b/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);