feat: simplest possible docstring search

nav.js

@@ -106,13 +106,14 @@ if (tse != null) {
 // Simple declaration search
 // -------------------------
 
-const declURL = new URL(`${siteRoot}decl.bmp`, window.location);
+const declURL = new URL(`${siteRoot}searchable_data.bmp`, window.location);
 const getDecls = (() => {
   let decls;
   return () => {
     if (!decls) decls = new Promise((resolve, reject) => {
         const req = new XMLHttpRequest();
-        req.addEventListener('load', () => resolve(loadDecls(req.responseText)));
+        req.responseType = 'json';
+        req.addEventListener('load', () => resolve(loadDecls(req.response)));
         req.addEventListener('error', () => reject());
         req.open('GET', declURL);
         req.send();

print_docs.py

@@ -757,9 +757,9 @@ def mk_export_map_entry(decl_name, filename, kind, is_meta, line, args, tp):
           'src_link': library_link(filename, line),
           'docs_link': f'{site_root}{filename.url}#{decl_name}'}
 
-def mk_export_db(loc_map, file_map):
+def mk_export_db(file_map):
   export_db = {}
-  for fn, decls in file_map.items():
+  for _, decls in file_map.items():
     for obj in decls:
       export_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['kind'], obj['is_meta'], obj['line'], obj['args'], obj['type'])
       export_db[obj['name']]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj)
@@ -774,6 +774,44 @@ def write_export_db(export_db):
   with gzip.GzipFile(html_root + 'export_db.json.gz', 'w') as zout:
     zout.write(json_str.encode('utf-8'))
 
+def mk_export_searchable_map_entry(filename_name, name, description, kind = '', attributes = []):
+  return {
+    'module': filename_name,
+    'name': name,
+    'description': description,
+    'kind': kind,
+    'attributes': attributes,
+  }
+
+def mk_export_searchable_db(file_map, tactic_docs):
+  export_searchable_db = []
+
+  for fn, decls in file_map.items():
+    filename_name = str(fn.url)
+    for obj in decls:
+      decl_entry = mk_export_searchable_map_entry(filename_name, obj['name'], obj['doc_string'], obj['kind'], obj['attributes'])
+      export_searchable_db.append(decl_entry)
+      for (cstr_name, _) in obj['constructors']:
+        cstr_entry = mk_export_searchable_map_entry(filename_name, cstr_name, obj['doc_string'], obj['kind'], obj['attributes'])
+        export_searchable_db.append(cstr_entry)
+      for (sf_name, _) in obj['structure_fields']:
+        sf_entry = mk_export_searchable_map_entry(filename_name, sf_name, obj['doc_string'], obj['kind'], obj['attributes'])
+        export_searchable_db.append(sf_entry)
+
+  for tactic in tactic_docs:
+    # category is the singular form of each docs webpage in 'General documentation'
+    # e.g. 'tactic' -> 'tactics.html'
+    tactic_entry_container_name = f"{tactic['category']}s.html"
+    tactic_entry = mk_export_searchable_map_entry(tactic_entry_container_name, tactic['name'], tactic['description'])
+    export_searchable_db.append(tactic_entry)
+
+  return export_searchable_db
+
+def write_export_searchable_db(searchable_data):
+  json_str = json.dumps(searchable_data)
+  with open_outfile('searchable_data.bmp') as out:
+    out.write(json_str)
+
 def main():
   bib = parse_bib_file(f'{local_lean_root}docs/references.bib')
   file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json()
@@ -785,7 +823,8 @@ def main():
   copy_css_and_js(html_root, use_symlinks=cl_args.l)
   copy_yaml_bib_files(html_root)
   copy_static_files(html_root)
-  write_export_db(mk_export_db(loc_map, file_map))
+  write_export_db(mk_export_db(file_map))
+  write_export_searchable_db(mk_export_searchable_db(file_map, tactic_docs))
   write_site_map(file_map)
 
 if __name__ == '__main__':

search.js

@@ -22,17 +22,22 @@ function matchCaseSensitive(declName, lowerDeclName, pat) {
     }
 }
 
-function loadDecls(declBmpCnt) {
-    return declBmpCnt.split('\n').map(d => [d, d.toLowerCase()]);
+function loadDecls(searchableDataCnt) {
+    return searchableDataCnt.map(({name, description}) => [name, name.toLowerCase(), description.toLowerCase()])
 }
 
-function getMatches(decls, pat, maxResults = 20) {
-    // const lowerPat = pat.toLowerCase();
-    // const caseSensitive = pat !== lowerPat;
+function getMatches(decls, pat, maxResults = 30) {
+    const lowerPats = pat.toLowerCase().split(/\s/g);
     const patNoSpaces = pat.replace(/\s/g, '');
     const results = [];
-    for (const [decl, lowerDecl] of decls) {
-        const err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
+    for (const [decl, lowerDecl, lowerDoc] of decls) {
+        let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces);
+
+        // match all words as substrings of docstring
+        if (!(err < 3) && pat.length > 3 && lowerPats.every(l => lowerDoc.indexOf(l) != -1)) {
+            err = 3;
+        }
+
         if (err !== undefined) {
             results.push({decl, err});
         }
@@ -41,6 +46,6 @@ function getMatches(decls, pat, maxResults = 20) {
 }
 
 if (typeof process === 'object') { // NodeJS
-    const declNames = loadDecls(require('fs').readFileSync('html/decl.bmp').toString());
-    console.log(getMatches(declNames, process.argv[2] || 'ltltle', 20));
+    const data = loadDecls(JSON.parse(require('fs').readFileSync('searchable_data.bmp').toString()));
+    console.log(getMatches(data, process.argv[2] || 'ltltle'));
 }