diff --git a/tabs/search.js b/tabs/search.js
index 676d8140c..cdafb8d45 100644
--- a/tabs/search.js
+++ b/tabs/search.js
@@ -67,8 +67,19 @@ tabNames = [
}
}
}
+
+ for (const [key, value] of this.setting2page) {
+ // for (const [key, value] of Object.entries(this.setting2page)) {
+ if ( key.toLowerCase().includes(keyword) ) {
+ for (const page of value) {
+ var rHTML = "
: {2}".format(page, page, key);
+ resultsDiv.innerHTML= resultsDiv.innerHTML.concat(rHTML);
+ }
+ }
+ }
+
for ( result of document.getElementsByClassName("searchResult") ) {
- result.addEventListener('click', simClick, false);
+ result.addEventListener('click', simClick, false);
}
}
@@ -106,6 +117,15 @@ tabNames = [
this.key2page.get(key).add(filename);
}
+ settings = htmlDoc.querySelectorAll('[data-setting]:not([data-setting=""])');
+ for (const element of settings) {
+ key = element.getAttribute('data-setting');
+ if (! this.setting2page.has(key) ) {
+ this.setting2page.set( key, new Set() );
+ }
+ this.setting2page.get(key).add(filename);
+ }
+
}
@@ -149,6 +169,7 @@ tabNames = [
TABS.search.initialize = function (callback) {
var self = this;
this.key2page = new Map();
+ this.setting2page = new Map();
this.messages;
if (GUI.active_tab != 'search') {