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
This commit is contained in:
tophf 2020-11-20 16:10:15 +03:00
parent 420480887e
commit 70e3ba15b7

View File

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