Latest build deployed.

_static/pretext/js/ptx_search.js

@@ -0,0 +1,112 @@
+function doSearch() {
+    // Get the search terms from the input text box
+    let terms = document.getElementById("ptxsearch").value;
+    // Where do we want to put the results?
+    let resultArea = document.getElementById("searchresults")
+    resultArea.innerHTML = "";  // clear out any previous results
+    // do the search using the provided index
+    let pageResult = ptx_lunr_idx.search(terms);
+    // Number the documents from first to last so we can order the results by their
+    // position in the book.
+    snum = 0;
+    for (let doc of ptx_lunr_docs) {
+        doc.snum = snum;
+        snum += 1;
+    }
+    // Transfer meta data from the document to the results to make it easy to add 
+    // our lists later.
+    augmentResults(pageResult, ptx_lunr_docs);
+    addResultToPage(pageResult, ptx_lunr_docs, resultArea);
+    MathJax.typeset();
+}
+
+// Find the entry for a search result in the original document index
+function findEntry(resultId, db) {
+    for (const page of db) {
+        if (page.id === resultId) {
+            return page;
+        }
+    }
+    return resultId;
+}
+
+function augmentResults(result, docs) {
+    for (let res of result) {
+        let info = findEntry(res.ref, docs);
+        res.number = info.number;
+        res.type = info.type;
+        res.title = info.title;
+        res.url = info.url;
+        res.level = info.level;
+        res.snum = info.snum;
+    }
+}
+
+
+function comparePosition(a, b) {
+    if (a.snum < b.snum) {
+        return -1;
+    }
+    if (a.snum > b.snum) {
+        return 1;
+    }
+    return 0;
+}
+
+function addResultToPage(result, docs, resultArea) {
+    let len = result.length
+    let high = result[Math.floor(len*0.25)].score;
+    let med = result[Math.floor(len*0.5)].score;
+    let low = result[Math.floor(len*0.75)].score;
+    // sort the results by their position in the book, not their score
+    result = result.sort(comparePosition)
+    let indent = "1";
+    let currIndent = indent;
+    let origResult = resultArea;
+    // Create list entries indenting as needed.  
+    for (const res of result) {
+        let link = document.createElement("a")
+        // add a class so we can colorize the results based on their rank in terms
+        // of search score.
+        if (res.score >= high) {
+            link.classList.add("high_result")
+        } else if (res.score >= med) {
+            link.classList.add("medium_result")
+        } else if (res.score >= low) {
+            link.classList.add("low_result")
+        }
+        currIndent = res.level;
+        if (currIndent > indent) {
+            indent = currIndent;
+            let ilist = document.createElement("ul")
+            ilist.classList.add("detailed_result");
+            resultArea.appendChild(ilist);
+            resultArea = ilist;
+        } else if (currIndent < indent) {
+            resultArea = origResult;
+            indent = currIndent;
+        }
+        let bullet = document.createElement("li")
+        bullet.style.marginTop = "5px";
+        link.href = `${res.url}`;
+        link.innerHTML = `${res.type} ${res.number} ${res.title}`;
+        bullet.appendChild(link)
+        let p = document.createElement("text");
+        p.innerHTML = `  (${res.score.toFixed(2)})`;
+        bullet.appendChild(p);
+        resultArea.appendChild(bullet);
+    }
+
+}
+
+
+function showHelp() {
+    let state = document.getElementById("helpme").style.display;
+    if (state == "none") {
+        document.getElementById("helpme").style.display = "block";
+        document.getElementById("helpbutt").innerHTML = "Hide Help"
+    } else {
+        document.getElementById("helpme").style.display = "none";
+        document.getElementById("helpbutt").innerHTML = "Show Help"
+    }
+}