From de9c9affd99cf49d1bf18f6f33f126637aaa99a8 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 17 Mar 2024 11:52:10 +0900
Subject: [PATCH] remove filePlay functionality

---
 assets/filePlay.js | 31 -------------------------------
 book.toml          |  4 ----
 2 files changed, 35 deletions(-)
 delete mode 100644 assets/filePlay.js

diff --git a/assets/filePlay.js b/assets/filePlay.js
deleted file mode 100644
index d2cd2a2..0000000
--- a/assets/filePlay.js
+++ /dev/null
@@ -1,31 +0,0 @@
-/**
- * Modifying the "Suggest an edit" button in mdbook
- * to link to the lean4 web editor
- */
-
-// The `i` element in the icon part of the edit button.
-const editButtonIcon = document.querySelector('#git-edit-button');
-editButtonIcon.className = 'fa fa-play';
-
-// The `a` element representing the edit button.
-const editButtonLink = editButtonIcon.parentElement;
-editButtonLink.title = 'Run on Lean 4 playground';
-editButtonLink.ariaLabel = editButtonLink.title;
-
-// Correct the `.md` extension to `.lean`.
-editButtonLink.href = editButtonLink.href.replace(/\.md$/, '.lean');
-
-// Correct the location of the directory where the Lean files are located.
-editButtonLink.href = editButtonLink.href.replace('/md/', '/Src/');
-
-editButtonLink.addEventListener('click', async function (e) {
-  e.preventDefault();
-
-  fetch(editButtonLink.href)
-    .then(response => response.text())
-    .then(body => {
-      const escaped_code = encodeURIComponent(body);
-      const url = `https://live.lean-lang.org/#code=${escaped_code}`;
-      open(url);
-    });
-});
\ No newline at end of file
diff --git a/book.toml b/book.toml
index b78ab5a..e42ee2a 100644
--- a/book.toml
+++ b/book.toml
@@ -12,14 +12,10 @@ build-dir = "book"
 
 [output.html]
 git-repository-url = "https://github.com/Seasawher/lean99"
-edit-url-template = "https://raw.githubusercontent.com/Seasawher/lean-book/main/{path}"
 additional-js = [
   # Add "Run on Lean4 Playground" button to each code block
   "assets/blockPlay.js",
 
-  # Add "Run on Lean4 Playground" button to each page
-  "assets/filePlay.js",
-
   # Improve search functionality
   "assets/fzf.umd.js",
   "assets/elasticlunr.js"