does enter enter search on random char

Author: EmileTrotignon

src/html_support_files/odoc_search.js

@@ -105,11 +105,6 @@ function focus_next_result() {
     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);
@@ -140,12 +135,13 @@ function handle_key_down(event) {
       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 `@`
+    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 ();