jon.recoil.org
this repo has no description
Search bar navigation (#1088)
authored by
Emile Trotignon
and committed by
GitHub
32506dfd
b7a7d675
+2
CHANGES.md
+2
CHANGES.md
···
8
8
- Separate compilation of interface and implementation files, using a new
9
9
`compile-src` command (@panglesd, #1067).
10
10
- Add clock emoji before `@since` tag (@yawaramin, #1089)
11
+
- Navigation for the search bar : use '/' to enter search, up and down arrows to
12
+
select a result, and enter to follow the selected link. (@EmileTrotignon, #1088)
11
13
12
14
### Changed
13
15
+1
-1
src/html/html_page.ml
+1
-1
src/html/html_page.ml
···
31
31
32
32
let html_of_search () =
33
33
let search_bar =
34
-
Html.(input ~a:[ a_class [ "search-bar" ]; a_placeholder "🔎 Search..." ] ())
34
+
Html.(input ~a:[ a_class [ "search-bar" ]; a_placeholder "🔎 Type '/' to search..." ] ())
35
35
in
36
36
let snake = Html.(div ~a:[ a_class [ "search-snake" ] ] []) in
37
37
let search_result = Html.div ~a:[ Html.a_class [ "search-result" ] ] [] in
+1
-1
src/html_support_files/odoc.css
+1
-1
src/html_support_files/odoc.css
+84
src/html_support_files/odoc_search.js
+84
src/html_support_files/odoc_search.js
···
64
64
wait();
65
65
worker.postMessage(ev.target.value);
66
66
});
67
+
68
+
69
+
/** Navigation */
70
+
71
+
let search_result_elt = document.querySelector(".search-result")
72
+
73
+
function search_results() {
74
+
return search_result_elt.children;
75
+
}
76
+
77
+
function enter_search() {
78
+
document.querySelector(".search-bar").focus();
79
+
}
80
+
81
+
function escape_search() {
82
+
document.activeElement.blur()
83
+
}
84
+
85
+
function focus_previous_result() {
86
+
let results = Array.from(search_results());
87
+
let current_focus = results.findIndex((elt) => (document.activeElement === elt));
88
+
if (current_focus === -1)
89
+
return;
90
+
else if (current_focus === 0)
91
+
enter_search();
92
+
else
93
+
results[current_focus - 1].focus();
94
+
}
95
+
96
+
function focus_next_result() {
97
+
let results = Array.from(search_results());
98
+
if (results.length === 0) return;
99
+
let current_focus = results.findIndex((elt) => (document.activeElement === elt));
100
+
if (current_focus === -1)
101
+
results[0].focus();
102
+
else if (current_focus + 1 === results.length)
103
+
return;
104
+
else
105
+
results[current_focus + 1].focus();
106
+
}
107
+
108
+
109
+
function is_searching() {
110
+
return (document.querySelectorAll(".odoc-search:focus-within").length > 0);
111
+
}
112
+
113
+
function is_typing() {
114
+
return (document.activeElement === document.querySelector(".search-bar"));
115
+
}
116
+
117
+
function handle_key_down(event) {
118
+
if (is_searching()) {
119
+
if (event.key === "ArrowUp") {
120
+
event.preventDefault();
121
+
focus_previous_result();
122
+
}
123
+
if (event.key === "ArrowDown") {
124
+
event.preventDefault();
125
+
focus_next_result();
126
+
}
127
+
if (event.key === "Escape") {
128
+
event.preventDefault();
129
+
escape_search();
130
+
}
131
+
}
132
+
if (!(is_typing())) {
133
+
let ascii = event.key.charCodeAt(0);
134
+
if (event.key === "/") {
135
+
event.preventDefault();
136
+
enter_search();
137
+
}
138
+
else if ( is_searching()
139
+
&& event.key.length === 1
140
+
&& ( (ascii >= 65 && ascii <= 90) // lowercase letter
141
+
|| (ascii >= 97 && ascii <= 122) // uppercase letter
142
+
|| (ascii >= 48 && ascii <= 57) // numbers
143
+
|| (ascii >= 32 && ascii <= 46) // ` ` to `.`
144
+
|| (ascii >= 58 && ascii <= 64)) // `:` to `@`
145
+
)
146
+
// We do not prevent default because we want the char to be added to the input
147
+
enter_search ();
148
+
}
149
+
}
150
+
document.addEventListener("keydown", handle_key_down);