Fix the problem where the background theme is not immediately changed…

… on Safari.

CHANGELOG.md

@@ -1,3 +1,6 @@
+# 1.7.1 (2023/11/25)
+- Fix the problem where the background theme is not immediately changed on Safari.
+
 # 1.7.0 (2023/11/24)
 - Fix the problem where finite-length music is unexpectedly fading on replay.
 - Enhance syntax highlighting.

public/js/editor.js

@@ -799,6 +799,8 @@ function openSettings() {
 function onThemeChange(event) {
   const id = event.srcElement.value;
   editor.setTheme(_themeIdToPath(id));
+  // Workaround for Safari: focus to apply background color.
+  editor.focus(); 
   saveEditorOptions();
 }
 
@@ -811,7 +813,6 @@ function onFontSizeChange(event) {
 function onWrapChange(event) {
   const wrap = event.srcElement.value;
   editor.setOption("wrap", wrap);
-  console.log(editor.getOption("wrap"));
   saveEditorOptions();
 }