From 3a977a94ca1548ff599a2b7373c6e3884fc9cb3f Mon Sep 17 00:00:00 2001
From: Jeremy Salwen <jeremysalwen@gmail.com>
Date: Sat, 28 Jan 2023 14:16:49 -0500
Subject: [PATCH] Fix issues with Search page impelementation

- Makes the autocomplete results highlight with up/down arrows.
- Allows you to unselect autocomplete results by using arrow keys.
- Fixed a bug in previous commits where enter did not take you to autocomplete result.
- Return now goes to the search page if no autocomplete result is selected.
- Search results table now properly wraps. (It would be nice to make it wider but I wasn't able to).
- Fixed a bug in the previous commit where docs were not showing, due to failure to copy a modified js file.
---
 DocGen4/Output/Search.lean   |  1 -
 DocGen4/Output/Template.lean |  2 +-
 static/declaration-data.js   |  1 +
 static/search.js             |  6 +++---
 static/style.css             | 22 ++++++++--------------
 5 files changed, 13 insertions(+), 19 deletions(-)

diff --git a/DocGen4/Output/Search.lean b/DocGen4/Output/Search.lean
index b748c7e..6a40f92 100644
--- a/DocGen4/Output/Search.lean
+++ b/DocGen4/Output/Search.lean
@@ -14,7 +14,6 @@ open scoped DocGen4.Jsx
 def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
   pure <|
     <main>
-      <a id="top"></a>
       <h1> Search Results </h1>
       <label for="search_page_query">Query:</label><input id="search_page_query" />
       <script>
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index f2b7409..ecff70c 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -48,7 +48,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
           <form action="https://google.com/search" method="get" id="search_form">
             <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
             <input type="text" name="q" autocomplete="off"/>&#32;
-            <button onclick="javascript: form.action='/search.html';">Search</button>
+            <button id="search_button" onclick="javascript: form.action='/search.html';">Search</button>
             <button>Google site search</button>
           </form>
         </header>
diff --git a/static/declaration-data.js b/static/declaration-data.js
index 8c4e42c..7aa899c 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -183,6 +183,7 @@ function getMatches(declarations, pattern, maxResults = undefined) {
     if (err !== undefined) {
       results.push({
         name,
+        doc,
         err,
         lowerName,
         lowerDoc,
diff --git a/static/search.js b/static/search.js
index e3d91ae..dc3b318 100644
--- a/static/search.js
+++ b/static/search.js
@@ -29,8 +29,8 @@ function handleSearchCursorUpDown(down) {
   if (sel) {
     sel.classList.remove("selected");
     const toSelect = down
-      ? sel.nextSibling || ac_results.firstChild
-      : sel.previousSibling || ac_results.lastChild;
+      ? sel.nextSibling 
+      : sel.previousSibling;
     toSelect && toSelect.classList.add("selected");
   } else {
     const toSelect = down ? ac_results.firstChild : ac_results.lastChild;
@@ -42,7 +42,7 @@ function handleSearchCursorUpDown(down) {
  * Perform search (when enter is pressed).
  */
 function handleSearchEnter() {
-  const sel = ac_results.querySelector(`.selected`) || ac_results.firstChild;
+  const sel = ac_results.querySelector(`.selected .result_link a`) || document.querySelector(`#search_button`);
   sel.click();
 }
 
diff --git a/static/style.css b/static/style.css
index 49e0486..efca72a 100644
--- a/static/style.css
+++ b/static/style.css
@@ -198,41 +198,35 @@ header header_filename {
     cursor: pointer;
 }
 
-#autocomplete_results .selected {
+#autocomplete_results .selected .result_link a {
     background: white;
     border-color: #f0a202;
 }
 
-#search_results a {
-    display: block;
-}
 
+#search_results {
+    display: table;
+    width: 100%;
+}
 #search_results[state="done"]:empty::before {
     content: '(no results)';
     font-style: italic;
 }
 
-#search_results {
-    width: 100%;
-    display: table;
-    table-layout: auto;
+#search_results .result_link, #search_results .result_doc {
+    border-bottom: 1px solid rgba(0, 0, 0, 0.8);
 }
 
 .search_result {
-    width: 100%;
     display: table-row;
 }
 
 .result_link, .result_doc {
     display: table-cell;
     overflow: hidden;
+    word-break: break-word;
 }
 
-#search_results .result_link, #search_results .result_doc {
-    display: table-cell;
-    overflow: hidden;
-    border-bottom: 1px solid rgba(0, 0, 0, 0.8);
-}
 main, nav {
     margin-top: calc(var(--header-height) + 1em);
 }