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..d0903a72 100644 --- a/theme/index.hbs +++ b/theme/index.hbs @@ -184,17 +184,12 @@ {{/if}} {{!-- - Discord への招待ボタン - 本来はアイコンを Discord のアイコンにすべきだが、mdbook が使用している FontAwesome はバージョンが 4.7.0 であり - Discord のアイコンが存在しない。そのため、コミュニティっぽいアイコンで代用している。 + 本来編集ページへのリンクだが、改造してファイル単位の実行ボタンにしている --}} - - - {{#if git_repository_edit_url}} - - + {{/if}}