From 207bf4cbaf46222cf91eca137d6d9e03fa5d243b Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Fri, 27 Sep 2024 02:15:40 +0900
Subject: [PATCH 1/2] =?UTF-8?q?=E4=B8=80=E7=9E=AC=20Suggest=20an=20edit=20?=
 =?UTF-8?q?=E3=83=9C=E3=82=BF=E3=83=B3=E3=81=8C=E8=A1=A8=E7=A4=BA=E3=81=95?=
 =?UTF-8?q?=E3=82=8C=E3=82=8B=E5=95=8F=E9=A1=8C=E3=82=92=E4=BF=AE=E6=AD=A3?=
 =?UTF-8?q?=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 assets/filePlay.js | 8 +++-----
 theme/index.hbs    | 7 +++++--
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/assets/filePlay.js b/assets/filePlay.js
index a56c9fdb..44bc892e 100644
--- a/assets/filePlay.js
+++ b/assets/filePlay.js
@@ -1,17 +1,15 @@
 /**
  * mdbook の "Suggest an edit" ボタンを改造し、
  * lean4 web editor へのリンクにしてしまう
+ *
+ * 一瞬元のアイコンが表示されるのを防ぐためにHTML側で上書きを行っていることに注意
  */
 function filePlay() {
   // 編集ボタンのアイコン部分の `i` 要素
-  const editButtonIcon = document.querySelector("#git-edit-button");
-  editButtonIcon.className = "fa fa-play";
-  editButtonIcon.id = "lean-play-button";
+  const editButtonIcon = document.querySelector("#lean-play-button");
 
   // 編集ボタンを表す `a` 要素
   const editButtonLink = editButtonIcon.parentElement;
-  editButtonLink.title = "Run on Lean 4 playground";
-  editButtonLink.ariaLabel = editButtonLink.title;
 
   // 拡張子が `.md` になっているので `.lean` に修正する
   editButtonLink.href = editButtonLink.href.replace(/\.md$/, ".lean");
diff --git a/theme/index.hbs b/theme/index.hbs
index eb1b4cca..261d24b7 100644
--- a/theme/index.hbs
+++ b/theme/index.hbs
@@ -191,10 +191,13 @@
                         <a href="https://discord.gg/p32ZfnVawh" title="Join our community" aria-label="Join community">
                             <i id="discord-invite-button" class="fa fa-comments-o"></i>
                         </a>
+                        {{!--
+                            本来編集ページへのリンクだが、改造してファイル単位の実行ボタンにしている
+                        --}}
                         {{#if git_repository_edit_url}}
-                        <a href="{{git_repository_edit_url}}" title="Suggest an edit" aria-label="Suggest an edit"
+                        <a href="{{git_repository_edit_url}}" title="Run on Lean 4 playground" aria-label="Run on Lean 4 playground"
                             target=_blank>
-                            <i id="git-edit-button" class="fa fa-edit"></i>
+                            <i id="lean-play-button" class="fa fa-play"></i>
                         </a>
                         {{/if}}
                     </div>

From 01a905789555790549d7469da7a40002d77e910a Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Fri, 27 Sep 2024 02:19:03 +0900
Subject: [PATCH 2/2] =?UTF-8?q?Discord=20=E3=81=B8=E3=81=AE=E3=83=AA?=
 =?UTF-8?q?=E3=83=B3=E3=82=AF=E3=83=9C=E3=82=BF=E3=83=B3=E3=82=92=E3=83=88?=
 =?UTF-8?q?=E3=83=83=E3=83=97=E3=81=AB=E8=A1=A8=E7=A4=BA=E3=81=97=E3=81=AA?=
 =?UTF-8?q?=E3=81=84?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theme/index.hbs | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/theme/index.hbs b/theme/index.hbs
index 261d24b7..d0903a72 100644
--- a/theme/index.hbs
+++ b/theme/index.hbs
@@ -183,14 +183,6 @@
                             <i id="git-repository-button" class="fa {{git_repository_icon}}"></i>
                         </a>
                         {{/if}}
-                        {{!--
-                            Discord への招待ボタン
-                            本来はアイコンを Discord のアイコンにすべきだが、mdbook が使用している FontAwesome はバージョンが 4.7.0 であり
-                            Discord のアイコンが存在しない。そのため、コミュニティっぽいアイコンで代用している。
-                        --}}
-                        <a href="https://discord.gg/p32ZfnVawh" title="Join our community" aria-label="Join community">
-                            <i id="discord-invite-button" class="fa fa-comments-o"></i>
-                        </a>
                         {{!--
                             本来編集ページへのリンクだが、改造してファイル単位の実行ボタンにしている
                         --}}