Add filters for search results based on kind.

This allows you to search defs, theorems, etc independently.

DocGen4/Output/Search.lean

@@ -15,7 +15,28 @@ def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
   pure <|
     <main>
       <h1> Search Results </h1>
-      <label for="search_page_query">Query:</label><input id="search_page_query" />
+      <label for="search_page_query">Query:</label>
+      <input id="search_page_query" />
+      <div id="kinds">
+        Allowed Kinds:
+        <input type="checkbox" id="def_checkbox" class="kind_checkbox" value="def" checked="checked" />
+        <label for="def_checkbox">def</label>
+        <input type="checkbox" id="theorem_checkbox" class="kind_checkbox" value="theorem" checked="checked" />
+        <label for="theorem_checkbox">theorem</label>
+        <input type="checkbox" id="inductive_checkbox" class="kind_checkbox" value="inductive" checked="checked" />
+        <label for="inductive_checkbox">inductive</label>
+        <input type="checkbox" id="structure_checkbox" class="kind_checkbox" value="structure" checked="checked" />
+        <label for="structure_checkbox">structure</label>
+        <input type="checkbox" id="class_checkbox" class="kind_checkbox" value="class" checked="checked" />
+        <label for="class_checkbox">class</label>
+        <input type="checkbox" id="instance_checkbox" class="kind_checkbox" value="instance" checked="checked" />
+        <label for="instance_checkbox">instance</label>
+        <input type="checkbox" id="axiom_checkbox" class="axiom_checkbox" value="axiom" checked="checked" />
+        <label for="axiom_checkbox">axiom</label>
+        <input type="checkbox" id="opaque_checkbox" class="kind_checkbox" value="opaque" checked="checked" />
+        <label for="opaque_checkbox">opaque</label>
+      </div>
+      
       <script>
         document.getElementById("search_page_query").value = new URL(window.location.href).searchParams.get("q")
       </script>

DocGen4/Output/ToJson.lean

@@ -9,6 +9,7 @@ open Lean
 
 structure JsonDeclaration where
   name : String
+  kind : String
   doc : String
   docLink : String
   sourceLink : String
@@ -76,10 +77,11 @@ def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM Js
 
 def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
   let name := info.getName.toString
+  let kind := info.getKind
   let doc := info.getDocString.getD ""
   let docLink ← declNameToLink info.getName
   let sourceLink ← getSourceUrl module info.getDeclarationRange
-  return { name, doc, docLink, sourceLink }
+  return { name, kind, doc, docLink, sourceLink }
 
 def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
     let mut jsonDecls := []

static/declaration-data.js

@@ -67,7 +67,7 @@ export class DeclarationDataCenter {
    * Search for a declaration.
    * @returns {Array<any>}
    */
-  search(pattern, strict = true, maxResults=undefined) {
+  search(pattern, strict = true, allowedKinds=undefined, 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, maxResults);
+      return getMatches(this.declarationData.declarations, pattern, allowedKinds, maxResults);
     }
   }
 
@@ -159,16 +159,23 @@ function matchCaseSensitive(declName, lowerDeclName, pattern) {
   }
 }
 
-function getMatches(declarations, pattern, maxResults = undefined) {
+function getMatches(declarations, pattern, allowedKinds = undefined, maxResults = undefined) {
   const lowerPats = pattern.toLowerCase().split(/\s/g);
   const patNoSpaces = pattern.replace(/\s/g, "");
   const results = [];
   for (const [_, {
     name,
+    kind,
     doc,
     docLink,
     sourceLink,
   }] of Object.entries(declarations)) {
+    // Apply "kind" filter
+    if (allowedKinds !== undefined) {
+      if (!allowedKinds.has(kind)) {
+        continue;
+      }
+    }
     const lowerName = name.toLowerCase();
     const lowerDoc = doc.toLowerCase();
     let err = matchCaseSensitive(name, lowerName, patNoSpaces);
@@ -183,6 +190,7 @@ function getMatches(declarations, pattern, maxResults = undefined) {
     if (err !== undefined) {
       results.push({
         name,
+        kind,
         doc,
         err,
         lowerName,

static/search.js

@@ -80,7 +80,7 @@ function removeAllChildren(node) {
 /**
  * Handle user input and perform search.
  */
-function handleSearch(dataCenter, err, ev, sr, maxResults, includedoc=false) {
+function handleSearch(dataCenter, err, ev, sr, maxResults, autocomplete) {
   const text = ev.target.value;
 
   // If no input clear all.
@@ -94,14 +94,25 @@ function handleSearch(dataCenter, err, ev, sr, maxResults, includedoc=false) {
   sr.setAttribute("state", "loading");
 
   if (dataCenter) {
-    const result = dataCenter.search(text, false, maxResults);
+    var allowedKinds;
+    if (!autocomplete) {
+      allowedKinds = new Set();
+      document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
+        {
+          if (checkbox.checked) {
+            allowedKinds.add(checkbox.value);
+          }
+        } 
+      );
+    }
+    const result = dataCenter.search(text, false, allowedKinds, maxResults);
 
     // in case user has updated the input.
     if (ev.target.value != text) return;
   
     // update autocomplete results
     removeAllChildren(sr);
-    for (const { name, doc, docLink } of result) {
+    for (const { name, kind, doc, docLink } of result) {
       const row = sr.appendChild(document.createElement("div"));
       row.classList.add("search_result")
       const linkdiv = row.appendChild(document.createElement("div"))
@@ -110,7 +121,7 @@ function handleSearch(dataCenter, err, ev, sr, maxResults, includedoc=false) {
       link.innerText = name;
       link.title = name;
       link.href = SITE_ROOT + docLink;
-      if (includedoc) {
+      if (!autocomplete) {
         const doctext = row.appendChild(document.createElement("div"));
         doctext.innerText = doc
         doctext.classList.add("result_doc")
@@ -129,15 +140,18 @@ function handleSearch(dataCenter, err, ev, sr, maxResults, includedoc=false) {
 DeclarationDataCenter.init()
   .then((dataCenter) => {
     // Search autocompletion.
-    SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS));
+    SEARCH_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS, true));
     if(SEARCH_PAGE_INPUT) {
-      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, true))
+      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false))
+      document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
+        checkbox.addEventListener("input", ev => SEARCH_PAGE_INPUT.dispatchEvent(new Event("input")))
+      );
       SEARCH_PAGE_INPUT.dispatchEvent(new Event("input"))
     }
   })
   .catch(e => {
-    SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS));
+    SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS,true ));
     if(SEARCH_PAGE_INPUT) {
-      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, true));
+      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false));
     }
   });