From 033003c6cbcd1b6e37163762b0da9ac307ade401 Mon Sep 17 00:00:00 2001 From: Jeremy Salwen Date: Wed, 25 Jan 2023 17:57:10 -0500 Subject: [PATCH] Add a search page to the docs. Now instead of clicking the "Google Site Search"' button, the user has the option of clicking the "Search" button, which will take them to a results page. Currently, the results are identical to the autocomplete results, but the number of results is not limited to 30. In the future, more information and search options could be added to this page to make a more powerful search. Fixes #107 --- DocGen4/Output.lean | 3 +++ DocGen4/Output/Search.lean | 28 ++++++++++++++++++++ DocGen4/Output/Template.lean | 2 +- DocGen4/Process/Hierarchy.lean | 1 + lakefile.lean | 1 + static/declaration-data.js | 6 ++--- static/search.js | 48 ++++++++++++++++++++++------------ static/style.css | 29 +++++++++++++------- 8 files changed, 88 insertions(+), 30 deletions(-) create mode 100644 DocGen4/Output/Search.lean diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 9d79088..ef495f5 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -12,6 +12,7 @@ import DocGen4.Output.Module import DocGen4.Output.NotFound import DocGen4.Output.Find import DocGen4.Output.SourceLinker +import DocGen4.Output.Search import DocGen4.Output.ToJson import DocGen4.Output.FoundationalTypes import DocGen4.LeanInk.Process @@ -35,11 +36,13 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do let notFoundHtml := ReaderT.run notFound config |>.toString let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString let navbarHtml := ReaderT.run navbar config |>.toString + let searchHtml := ReaderT.run search config |>.toString let docGenStatic := #[ ("style.css", styleCss), ("declaration-data.js", declarationDataCenterJs), ("nav.js", navJs), ("how-about.js", howAboutJs), + ("search.html", searchHtml), ("search.js", searchJs), ("mathjax-config.js", mathjaxConfigJs), ("instances.js", instancesJs), diff --git a/DocGen4/Output/Search.lean b/DocGen4/Output/Search.lean new file mode 100644 index 0000000..b748c7e --- /dev/null +++ b/DocGen4/Output/Search.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2023 Jeremy Salwen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jeremy Salwen +-/ +import DocGen4.Output.ToHtmlFormat +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <| + pure <| +
+ +

Search Results

+ + +
+
+
+ +end Output +end DocGen4 diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 2c7ea8a..f2b7409 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -45,10 +45,10 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d

Documentation

{title}

- -- TODO: Replace this form with our own search
+
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 01b3ba0..86d2be0 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/DocGen4/Process/Hierarchy.lean @@ -89,6 +89,7 @@ def baseDirBlackList : HashSet String := "find", "how-about.js", "index.html", + "search.html", "foundational_types.html", "mathjax-config.js", "navbar.html", diff --git a/lakefile.lean b/lakefile.lean index 9a8b32f..f558b8b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -94,6 +94,7 @@ library_facet docs (lib) : FilePath := do basePath / "index.html", basePath / "404.html", basePath / "navbar.html", + basePath / "search.html", basePath / "find" / "index.html", basePath / "find" / "find.js", basePath / "src" / "alectryon.css", diff --git a/static/declaration-data.js b/static/declaration-data.js index 953edf2..8c4e42c 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -67,7 +67,7 @@ export class DeclarationDataCenter { * Search for a declaration. * @returns {Array} */ - search(pattern, strict = true) { + search(pattern, strict = true, maxResults=undefined) { if (!pattern) { return []; } @@ -75,7 +75,7 @@ export class DeclarationDataCenter { let decl = this.declarationData.declarations[pattern]; return decl ? [decl] : []; } else { - return getMatches(this.declarationData.declarations, pattern); + return getMatches(this.declarationData.declarations, pattern, maxResults); } } @@ -159,7 +159,7 @@ function matchCaseSensitive(declName, lowerDeclName, pattern) { } } -function getMatches(declarations, pattern, maxResults = 30) { +function getMatches(declarations, pattern, maxResults = undefined) { const lowerPats = pattern.toLowerCase().split(/\s/g); const patNoSpaces = pattern.replace(/\s/g, ""); const results = []; diff --git a/static/search.js b/static/search.js index 074d8bc..835bfca 100644 --- a/static/search.js +++ b/static/search.js @@ -4,27 +4,36 @@ import { DeclarationDataCenter } from "./declaration-data.js"; +// Search form and input in the upper right toolbar const SEARCH_FORM = document.querySelector("#search_form"); const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]"); -// Create an `div#search_results` to hold all search results. -let sr = document.createElement("div"); -sr.id = "search_results"; -SEARCH_FORM.appendChild(sr); +// Search form on the /search.html_page. These may be null. +const SEARCH_PAGE_INPUT = document.querySelector("#search_page_query") +const SEARCH_RESULTS = document.querySelector("#search_results") + +// Max results to show for autocomplete or /search.html page. +const AC_MAX_RESULTS = 30 +const SEARCH_PAGE_MAX_RESULTS = undefined + +// Create an `div#autocomplete_results` to hold all autocomplete results. +let ac_results = document.createElement("div"); +ac_results.id = "autocomplete_results"; +SEARCH_FORM.appendChild(ac_results); /** - * Attach `selected` class to the the selected search result. + * Attach `selected` class to the the selected autocomplete result. */ function handleSearchCursorUpDown(down) { - const sel = sr.querySelector(`.selected`); + const sel = ac_results.querySelector(`.selected`); if (sel) { sel.classList.remove("selected"); const toSelect = down - ? sel.nextSibling || sr.firstChild - : sel.previousSibling || sr.lastChild; + ? sel.nextSibling || ac_results.firstChild + : sel.previousSibling || ac_results.lastChild; toSelect && toSelect.classList.add("selected"); } else { - const toSelect = down ? sr.firstChild : sr.lastChild; + const toSelect = down ? ac_results.firstChild : ac_results.lastChild; toSelect && toSelect.classList.add("selected"); } } @@ -33,12 +42,12 @@ function handleSearchCursorUpDown(down) { * Perform search (when enter is pressed). */ function handleSearchEnter() { - const sel = sr.querySelector(`.selected`) || sr.firstChild; + const sel = ac_results.querySelector(`.selected`) || ac_results.firstChild; sel.click(); } /** - * Allow user to navigate search results with up/down arrow keys, and choose with enter. + * Allow user to navigate autocomplete results with up/down arrow keys, and choose with enter. */ SEARCH_INPUT.addEventListener("keydown", (ev) => { switch (ev.key) { @@ -71,7 +80,7 @@ function removeAllChildren(node) { /** * Handle user input and perform search. */ -function handleSearch(dataCenter, err, ev) { +function handleSearch(dataCenter, err, ev, sr, maxResults) { const text = ev.target.value; // If no input clear all. @@ -85,12 +94,12 @@ function handleSearch(dataCenter, err, ev) { sr.setAttribute("state", "loading"); if (dataCenter) { - const result = dataCenter.search(text, false); + const result = dataCenter.search(text, false, maxResults); // in case user has updated the input. if (ev.target.value != text) return; - // update search results + // update autocomplete results removeAllChildren(sr); for (const { name, docLink } of result) { const d = sr.appendChild(document.createElement("a")); @@ -111,8 +120,15 @@ function handleSearch(dataCenter, err, ev) { DeclarationDataCenter.init() .then((dataCenter) => { // Search autocompletion. - SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev)); + SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS)); + if(SEARCH_PAGE_INPUT) { + SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS)) + SEARCH_PAGE_INPUT.dispatchEvent(new Event("input")) + } }) .catch(e => { - SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev)); + SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS)); + if(SEARCH_PAGE_INPUT) { + SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS)); + } }); diff --git a/static/style.css b/static/style.css index 2944e99..0701500 100644 --- a/static/style.css +++ b/static/style.css @@ -116,7 +116,7 @@ header { :root { --header-side-padding: 1ex; } #search_form button { display: none; } #search_form input { width: 100%; } - header #search_results { + header #autocomplete_results { left: 1ex; right: 1ex; width: inherit; @@ -146,7 +146,7 @@ header header_filename { } /* inserted by nav.js */ -#search_results { +#autocomplete_results { position: absolute; top: var(--header-height); right: calc(var(--header-side-padding)); @@ -160,15 +160,15 @@ header header_filename { max-height: calc(100vh - var(--header-height)); } -#search_results:empty { +#autocomplete_results:empty { display: none; } -#search_results[state="loading"]:empty { +#autocomplete_results[state="loading"]:empty { display: block; cursor: progress; } -#search_results[state="loading"]:empty::before { +#autocomplete_results[state="loading"]:empty::before { display: block; content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; padding: 1ex; @@ -179,17 +179,17 @@ header header_filename { 100% { transform: translate(-100%, 0); } } -#search_results[state="done"]:empty { +#autocomplete_results[state="done"]:empty { display: block; text-align: center; padding: 1ex; } -#search_results[state="done"]:empty::before { +#autocomplete_results[state="done"]:empty::before { content: '(no results)'; font-style: italic; } -#search_results a { +#autocomplete_results a { display: block; color: inherit; padding: 1ex; @@ -197,11 +197,20 @@ header header_filename { padding-left: 0.5ex; cursor: pointer; } -#search_results .selected { +#autocomplete_results .selected { background: white; border-color: #f0a202; } +#search_results a { + display: block; +} + +#search_results[state="done"]:empty::before { + content: '(no results)'; + font-style: italic; +} + main, nav { margin-top: calc(var(--header-height) + 1em); } @@ -476,7 +485,7 @@ main h2, main h3, main h4, main h5, main h6 { } .imports li, code, .decl_header, .attributes, .structure_field_info, - .constructor, .instances li, .equation, #search_results div, + .constructor, .instances li, .equation, #autocomplete_results div, .structure_ext_ctor { font-family: 'Source Code Pro', monospace; }