Move themes directly into HTML

Author: GuillaumeGomez

util/gh-pages/index.html

@@ -30,7 +30,13 @@
         <div class="settings-icon" tabindex="-1"></div>
         <div class="settings-menu" tabindex="-1">
             <div class="setting-radio-name">Theme</div>
-            <select id="theme-choice" onchange="setTheme(this.value, true)"></select>
+            <select id="theme-choice" onchange="setTheme(this.value, true)">
+                <option value="ayu">Ayu</option>
+                <option value="coal">Coal</option>
+                <option value="light">Light</option>
+                <option value="navy">Navy</option>
+                <option value="rust">Rust</option>
+            </select>
             <label>
                 <input type="checkbox" id="disable-shortcuts" onchange="changeSetting(this)">
                 <span>Disable keyboard shortcuts</span>

util/gh-pages/script.js

@@ -604,17 +604,6 @@ function handleBlur(event) {
 }
 
 function generateSettings() {
-    const THEMES = ["Ayu", "Coal", "Light", "Navy", "Rust"];
-    const themesElem = document.getElementById("theme-choice");
-    let children = '';
-
-    for (const theme of THEMES) {
-        const id = theme.toLowerCase();
-        children += `<option value="${id}">${theme}</option>`;
-    }
-    themesElem.innerHTML = children;
-    themesElem.onblur = handleBlur;
-
     const settings = document.getElementById("settings-dropdown");
     const settingsButton = settings.querySelector(".settings-icon")
     settingsButton.onclick = () => settings.classList.toggle("open");