From dec486ef462881801b70602407e9a1f0b3f0d4c7 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Wed, 27 Mar 2024 21:17:23 +0900
Subject: [PATCH] add "run on Lean4 Playground" button to code blocks

---
 assets/blockPlay.js | 23 +++++++++++++++++++++++
 book.toml           |  5 ++++-
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 assets/blockPlay.js

diff --git a/assets/blockPlay.js b/assets/blockPlay.js
new file mode 100644
index 0000000..ac73b5c
--- /dev/null
+++ b/assets/blockPlay.js
@@ -0,0 +1,23 @@
+Array.from(document.querySelectorAll(".language-lean")).forEach(function (code_block) {
+  let pre_block = code_block.parentElement;
+
+  // create a link to lean4 web editor
+  let escaped_code = encodeURIComponent(code_block.textContent);
+  let url = `https://live.lean-lang.org/#code=${escaped_code}`;
+
+  // create a button
+  let buttons = pre_block.querySelector(".buttons");
+  let leanWebButton = document.createElement('button');
+  leanWebButton.className = 'fa fa-external-link lean-web-button';
+  leanWebButton.hidden = true;
+  leanWebButton.title = 'Run on lean4 playground';
+  leanWebButton.setAttribute('aria-label', leanWebButton.title);
+
+  // insert the button
+  buttons.insertBefore(leanWebButton, buttons.firstChild);
+
+  // open the link when the button is clicked
+  leanWebButton.addEventListener('click', function (e) {
+    open(url);
+  });
+});
\ No newline at end of file
diff --git a/book.toml b/book.toml
index cfd8de7..9cd1486 100644
--- a/book.toml
+++ b/book.toml
@@ -6,4 +6,7 @@ src = "."
 title = "Metaprogramming in Lean 4"
 
 [output.html]
-git-repository-url = "https://github.com/leanprover-community/lean4-metaprogramming-book"
\ No newline at end of file
+git-repository-url = "https://github.com/leanprover-community/lean4-metaprogramming-book"
+additional-js = [
+  "assets/blockPlay.js", # Add "Run on Lean4 Playground" button to each code block
+]
\ No newline at end of file