add lookup popup scaling option

options.html

@@ -17,6 +17,7 @@
 <input id="fixedwidth" type="checkbox" name=fixedwidth class=panel-formElements-item/><label for=fixedwidth class=panel-formElements-item>Fixed width</label><br>
 <input id="fixedwidthpositioning" type="checkbox" name=fixedwidthpositioning class=panel-formElements-item/><label for=fixedwidthpositioning class=panel-formElements-item>Position as though fixed width</label><br>
 <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><br>
+<input id="scale" type="number" min="0.1" max="64" value="1" name=scale class=panel-formElements-item step="0.1"/><label for=scale class=panel-formElements-item>Lookup popup scale</label><br>
 <p>This extension uses JMdict, which is Copyright © 2017 The Electronic Dictionary Research and Development Group and licensed under the <a href="https://creativecommons.org/licenses/by-sa/3.0/">CC BY-SA 3.0</a> license.</p>
 <p>This extension is otherwise licensed under the <a href="https://www.apache.org/licenses/LICENSE-2.0">Apache License, version 2.0</a>.</p>
 <div><p>Meanings of abbreviations follow. From JMdict.<p>

options.js

@@ -3,6 +3,7 @@ function restoreListeners()
     document.querySelector("#enabled").addEventListener("change", setOptions);
     document.querySelector("#compact").addEventListener("change", setOptions);
     document.querySelector("#length").addEventListener("change", setOptions);
+    document.querySelector("#scale").addEventListener("change", setOptions);
     document.querySelector("#fixedwidth").addEventListener("change", setOptions);
     document.querySelector("#fixedwidthpositioning").addEventListener("change", setOptions);
     document.querySelector("#superborder").addEventListener("change", setOptions);
@@ -13,6 +14,7 @@ function removeListeners()
     document.querySelector("#enabled").removeEventListener("change", setOptions);
     document.querySelector("#compact").removeEventListener("change", setOptions);
     document.querySelector("#length").removeEventListener("change", setOptions);
+    document.querySelector("#scale").addEventListener("change", setOptions);
     document.querySelector("#fixedwidth").removeEventListener("change", setOptions);
     document.querySelector("#fixedwidthpositioning").removeEventListener("change", setOptions);
     document.querySelector("#superborder").addEventListener("change", setOptions);
@@ -33,6 +35,7 @@ async function restoreOptions()
         let enabled = await getvar("enabled", false);
         let compact = await getvar("compact", true);
         let length = await getvar("length", 25);
+        let scale = await getvar("scale", 1);
         let fixedwidth = await getvar("fixedwidth", false);
         let fixedwidthpositioning = await getvar("fixedwidthpositioning", false);
         let superborder = await getvar("superborder", false);
@@ -41,6 +44,7 @@ async function restoreOptions()
         document.querySelector("#enabled").checked = enabled?true:false;
         document.querySelector("#compact").checked = compact?true:false;
         document.querySelector("#length").value = length?length:25;
+        document.querySelector("#scale").value = scale?scale:1;
         document.querySelector("#fixedwidth").checked = fixedwidth?true:false;
         document.querySelector("#fixedwidthpositioning").checked = fixedwidthpositioning?true:false;
         document.querySelector("#superborder").checked = superborder?true:false;
@@ -61,11 +65,15 @@ function setOptions()
     let length = parseInt(document.querySelector("#length").value, 10);
     if(!length) // NaN is falsy
         length = 25;
+    let scale = Number(document.querySelector("#scale").value);
+    if(!scale) // NaN is falsy
+        scale = 1;
     browser.storage.local.set(
     {
         enabled: document.querySelector("#enabled").checked,
         compact: document.querySelector("#compact").checked,
         length: length,
+        scale: scale,
         fixedwidth: document.querySelector("#fixedwidth").checked,
         fixedwidthpositioning: document.querySelector("#fixedwidthpositioning").checked,
         superborder: document.querySelector("#superborder").checked,

texthook.js

@@ -30,6 +30,7 @@ fixedwidth: false,
 fixedwidthpositioning: false,
 superborder: false,
 showoriginal: true,
+scale: 1,
 };
 
 let last_time_display = Date.now();
@@ -100,9 +101,11 @@ function display_div (middle, x, y, time)
         mydoc.body.appendChild(outer);
     }
     
+    if(settings.scale != 1 && settings.scale > 0 && settings.scale < 64)
+        styletext += " transform-origin: top left; transform: scale(" + Number(settings.scale) + ");";
+    
     outer.style = styletext;
-    
-    
+        
     let mywidth = 600;
     if(!settings.fixedwidthpositioning)
         mywidth = outer.offsetWidth;
@@ -569,7 +572,7 @@ browser.storage.onChanged.addListener((updates, storageArea) =>
     {
         let option = setting[0];
         let value = setting[1];
-        if(["enabled","compact","length","fixedwidth","fixedwidthpositioning","superborder","showoriginal"].includes(option))
+        if(["enabled","compact","length","fixedwidth","fixedwidthpositioning","superborder","showoriginal","scale"].includes(option))
             settings[option] = value.newValue;
     }
     if(!settings.enabled && exists_div())