From 70e3ba15b7c42d6ae7f4ff6ec0d268a38d31c487 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Fri, 20 Nov 2020 16:10:15 +0300
Subject: [PATCH] use 'default' internally for the default theme element

* the pref won't be influenced by the current UI language
* also reset to 'default' if failed to load the theme's css file
---
 edit/edit.js | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/edit/edit.js b/edit/edit.js
index 7468c47d..10981164 100644
--- a/edit/edit.js
+++ b/edit/edit.js
@@ -186,6 +186,10 @@ lazyInit();
         // preload the theme so CodeMirror can use the correct metrics
         el.href = `vendor/codemirror/theme/${theme}.css`;
         el.on('load', resolve, {once: true});
+        el.on('error', () => {
+          prefs.set('editor.theme', 'default');
+          resolve();
+        }, {once: true});
       }
     });
   }
@@ -206,8 +210,10 @@ lazyInit();
   }
 
   function buildThemeElement() {
-    CODEMIRROR_THEMES.unshift(chrome.i18n.getMessage('defaultTheme'));
-    $('#editor.theme').append(...CODEMIRROR_THEMES.map(s => $create('option', s)));
+    const elOptions = [chrome.i18n.getMessage('defaultTheme'), ...CODEMIRROR_THEMES]
+      .map(s => $create('option', s));
+    elOptions[0].value = 'default';
+    $('#editor.theme').append(...elOptions);
     // move the theme after built-in CSS so that its same-specificity selectors win
     document.head.appendChild($('#cm-theme'));
   }