Skip to content

Instantly share code, notes, and snippets.

@felixr

felixr/generate_search_index.js

Created December 10, 2020 17:10
Show Gist options
  • Save felixr/c1935e6c66fddd10aa7cc01db67bbff4 to your computer and use it in GitHub Desktop.
Save felixr/c1935e6c66fddd10aa7cc01db67bbff4 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. felixr revised this gist Dec 10, 2020. 1 changed file with 3 additions and 0 deletions.
    3 changes: 3 additions & 0 deletions generate_search_index.js
    View file
    Original file line number Diff line number Diff line change
    @@ -1,4 +1,7 @@
    function dtype(t) { return t=="function" ? "Function" : (t=="macro" ? "Macro": "Builtin");}

    let s = "";

    for (let b of document.querySelectorAll('.binding')) {
    s += `INSERT OR IGNORE INTO searchIndex(name, type, path) VALUES ("${b.firstChild.id}","${dtype(b.children[1].innerText)}","api/index.html#${b.firstChild.id}");\n`;
    }
  2. felixr created this gist Dec 10, 2020.
    5 changes: 5 additions & 0 deletions generate_search_index.js
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,5 @@
    let s = "";
    for (let b of document.querySelectorAll('.binding')) {
    s += `INSERT OR IGNORE INTO searchIndex(name, type, path) VALUES ("${b.firstChild.id}","${dtype(b.children[1].innerText)}","api/index.html#${b.firstChild.id}");\n`;
    }
    s