Merge pull request #893 from lean-ja/suggest-edit

一瞬 Suggest an edit ボタンが表示される問題を修正する

Author: Seasawher

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");

theme/index.hbs

@@ -184,17 +184,12 @@
                         </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>
                         {{#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>