add superborder option and stuff

background-script.js

@@ -719,13 +719,13 @@ function lookup_indirect(text, time, divexisted)
     // try to look up successively shorter substrings of text
     // deconjugate() returns possible deconjugations, one of which has zero deconjugations, i.e. the plain text
     // build_lookup_comb looks for dictionary definitions matching any deconjugation, returning a list of them
-    console.log("trying to look up " + text);
+    //console.log("trying to look up " + text);
     let forms = deconjugate(text);
     let result = build_lookup_comb(forms);
     while(result === undefined && text.length > 0)
     {
         text = text.substring(0, text.length-1);
-        console.log("trying to look up " + text);
+        //console.log("trying to look up " + text);
         forms = deconjugate(text);
         result = build_lookup_comb(forms);
     }

options.html

@@ -12,6 +12,7 @@
 <div class="panel-section panel-section-formElements browser-style">
 <input id="enabled" type="checkbox" name=enabled class=panel-formElements-item/><label for=enabled class=panel-formElements-item>Enabled</label>
 <input id="compact" type="checkbox" name=compact class=panel-formElements-item/><label for=compact class=panel-formElements-item>Compact</label>
+<input id="superborder" type="checkbox" name=superborder class=panel-formElements-item/><label for=superborder class=panel-formElements-item>Super border</label>
 <input id="fixedwidth" type="checkbox" name=fixedwidth class=panel-formElements-item/><label for=fixedwidth class=panel-formElements-item>Fixed width</label>
 <input id="fixedwidthpositioning" type="checkbox" name=fixedwidthpositioning class=panel-formElements-item/><label for=fixedwidthpositioning class=panel-formElements-item>Position as though fixed width</label>
 <input id="length" type="number" min="6" max="100" value="25" name=length class=panel-formElements-item/><label for=length class=panel-formElements-item>Search length (characters) (default 25, sane values are from 25 to 50)</label>

options.js

@@ -5,6 +5,7 @@ function restoreListeners()
     document.querySelector("#length").addEventListener("change", setOptions);
     document.querySelector("#fixedwidth").addEventListener("change", setOptions);
     document.querySelector("#fixedwidthpositioning").addEventListener("change", setOptions);
+    document.querySelector("#superborder").addEventListener("change", setOptions);
 }
 function removeListeners()
 {
@@ -13,33 +14,33 @@ function removeListeners()
     document.querySelector("#length").removeEventListener("change", setOptions);
     document.querySelector("#fixedwidth").removeEventListener("change", setOptions);
     document.querySelector("#fixedwidthpositioning").removeEventListener("change", setOptions);
+    document.querySelector("#superborder").addEventListener("change", setOptions);
 }
 
 async function restoreOptions()
 {
     try
     {
-        let enabled = (await browser.storage.local.get("enabled")).enabled;
+        async function getvar(name, defval)
-        if(enabled == undefined)
+        {
-            enabled = false;
+            let temp = (await browser.storage.local.get(name))[name];
-        let compact = (await browser.storage.local.get("compact")).compact;
+            if(temp == undefined)
-        if(compact == undefined)
+                temp = defval;
-            compact = true;
+            return temp;
-        let length = (await browser.storage.local.get("length")).length;
+        }
-        if(length == undefined)
+        let enabled = await getvar("enabled", false);
-            length = 25;
+        let compact = await getvar("compact", true);
-        let fixedwidth = (await browser.storage.local.get("fixedwidth")).fixedwidth;
+        let length = await getvar("length", 25);
-        if(fixedwidth == undefined)
+        let fixedwidth = await getvar("fixedwidth", false);
-            fixedwidth = false;
+        let fixedwidthpositioning = await getvar("fixedwidthpositioning", false);
-        let fixedwidthpositioning = (await browser.storage.local.get("fixedwidthpositioning")).fixedwidthpositioning;
+        let superborder = await getvar("superborder", true);
-        if(fixedwidthpositioning == undefined)
-            fixedwidthpositioning = false;
         removeListeners();
         document.querySelector("#enabled").checked = enabled?true:false;
         document.querySelector("#compact").checked = compact?true:false;
         document.querySelector("#length").value = length?length:25;
         document.querySelector("#fixedwidth").checked = fixedwidth?true:false;
         document.querySelector("#fixedwidthpositioning").checked = fixedwidthpositioning?true:false;
+        document.querySelector("#superborder").checked = superborder?true:false;
     }
     catch (error){}
     removeListeners();
@@ -58,6 +59,7 @@ function setOptions()
         length: length,
         fixedwidth: document.querySelector("#fixedwidth").checked,
         fixedwidthpositioning: document.querySelector("#fixedwidthpositioning").checked,
+        superborder: document.querySelector("#superborder").checked,
     });
 }
 

texthook.js

@@ -28,6 +28,7 @@ compact: true,
 length: 25,
 fixedwidth: false,
 fixedwidthpositioning: false,
+superborder: false,
 };
 
 let last_time_display = Date.now();
@@ -47,8 +48,14 @@ function delete_div ()
 
 function display_div (middle, x, y, time)
 {
+    let bordercolor = undefined;
+    if(settings.superborder)
+        bordercolor = "white";
+    else
+        bordercolor = "#CCC";
+    
     middle.style = "background-color: #111; border-radius: 2.5px; border: 1px solid #111;";
-    middle.firstChild.style = "border: 1px solid white; border-radius: 2px; padding: 2px; background-color: #111; color: #CCC; font-family: Arial, sans-serif; font-size: 13px; text-align: left;";
+    middle.firstChild.style = "border: 1px solid " + bordercolor + "; border-radius: 2px; padding: 2px; background-color: #111; color: #CCC; font-family: Arial, sans-serif; font-size: 13px; text-align: left;";
     
     let find_root = window;
     let newx = x;
@@ -69,8 +76,12 @@ function display_div (middle, x, y, time)
         styletext += "width: 600px; "
     else
         styletext += "max-width: 600px; "
-    styletext += "position: absolute; top: 0; left: 0;";
+    styletext += "position: absolute; top: 0; left: 0; ";
-    styletext += "background-color: white; border-radius: 3px; border: 1px solid white; z-index: 100000;";
+    
+    if(settings.superborder)
+        styletext += "background-color: " + bordercolor + "; border-radius: 3px; border: 1px solid " + bordercolor + "; z-index: 100000;";
+    else
+        styletext += "border-radius: 3px; background-color: #111; z-index: 100000;";
     
     let other = mydoc.body.getElementsByClassName(div_class);
     let outer = undefined;
@@ -476,21 +487,19 @@ async function settings_reload()
 {
     try
     {
-        settings.enabled = (await browser.storage.local.get("enabled")).enabled;
+        async function getvar(name, defval)
-        if(settings.enabled == undefined)
+        {
-            settings.enabled = false;
+            let temp = (await browser.storage.local.get(name))[name];
-        settings.compact = (await browser.storage.local.get("compact")).compact;
+            if(temp == undefined)
-        if(settings.compact == undefined)
+                temp = defval;
-            settings.compact = true;
+            settings[name] = temp;
-        settings.length = (await browser.storage.local.get("length")).length;
+        }
-        if(!settings.length)
+        getvar("enabled", false);
-            settings.length = 25;
+        getvar("compact", true);
-        settings.fixedwidth = (await browser.storage.local.get("fixedwidth")).fixedwidth;
+        getvar("length", 25);
-        if(!settings.fixedwidth)
+        getvar("fixedwidth", false);
-            settings.fixedwidth = false;
+        getvar("fixedwidthpositioning", false);
-        settings.fixedwidthpositioning = (await browser.storage.local.get("fixedwidthpositioning")).fixedwidthpositioning;
+        getvar("superborder", true);
-        if(!settings.fixedwidthpositioning)
-            settings.fixedwidthpositioning = false;
         
         if(!settings.enabled && exists_div())
             delete_div();