From f9f66a2472c5ab45a2653772b26838bf3a01ce13 Mon Sep 17 00:00:00 2001
From: Mitsutaka Okazaki <okaxaki@users.noreply.github.com>
Date: Sat, 25 Nov 2023 14:12:39 +0900
Subject: [PATCH] Fix the problem where the background theme is not 
 immediately changed on Safari.

---
 CHANGELOG.md        | 3 +++
 public/js/editor.js | 3 ++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 91f10f5..bb6686e 100644
--- a/CHANGELOG.md
+++ b/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.
diff --git a/public/js/editor.js b/public/js/editor.js
index 181bdaa..89259d5 100644
--- a/public/js/editor.js
+++ b/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();
 }