Message assertion

.github/workflows/deploy.yml

@@ -37,7 +37,7 @@ jobs:
       - name: setup mdBook
         uses: peaceiris/actions-mdbook@v1
         with:
-          mdbook-version: '0.4.32'
+          mdbook-version: '0.4.35'
 
       - name: build html from markdown
         run: mdbook build

assets/blockPlay.js

@@ -0,0 +1,27 @@
+/**
+ * Add a button to jump to the Lean 4 web playground within the Lean 4 code block
+ */
+function blockPlay() {
+  const array = Array.from(document.querySelectorAll(".language-lean"));
+  for (const code_block of array) {
+    const pre_block = code_block.parentElement;
+
+    const escaped_code = encodeURIComponent(code_block.textContent);
+    const url = `https://live.lean-lang.org/#code=${escaped_code}`;
+
+    const buttons = pre_block.querySelector(".buttons");
+    const 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);
+
+    buttons.insertBefore(leanWebButton, buttons.firstChild);
+
+    leanWebButton.addEventListener("click", (e) => {
+      open(url);
+    });
+  }
+}
+
+blockPlay();

assets/filePlay.js

@@ -0,0 +1,27 @@
+/** Modifies the "Suggest an edit" button of mdbook,
+
+* changing it to a link to the Lean4 web editor.
+* Note that the modification is done on the HTML side to prevent the original icon from appearing for a moment.
+*/
+function filePlay() {
+  const playButtonIcon = document.querySelector("#lean-play-button");
+
+  const playButtonLink = playButtonIcon.parentElement;
+
+  playButtonLink.href = playButtonLink.href.replace(/\.md$/, ".lean");
+
+  playButtonLink.href = playButtonLink.href.replace(
+    "/md/",
+    "/lean/",
+  );
+
+  fetch(playButtonLink.href)
+    .then((response) => response.text())
+    .then((body) => {
+      const escaped_code = encodeURIComponent(body);
+      const url = `https://live.lean-lang.org/#code=${escaped_code}`;
+      playButtonLink.href = url;
+    });
+}
+
+filePlay();

assets/pagetoc.css

@@ -0,0 +1,109 @@
+:root {
+  --toc-width: 270px;
+  --center-content-toc-shift: calc(-1 * var(--toc-width) / 2);
+}
+
+.nav-chapters {
+  /* adjust width of buttons that bring to the previous or the next page */
+  min-width: 50px;
+}
+
+.previous {
+  /*
+  adjust the space between the left sidebar or the left side of the screen
+  and the button that leads to the previous page
+  */
+  margin-left: var(--page-padding);
+}
+
+@media only screen {
+  main {
+    display: flex;
+  }
+
+  @media (max-width: 1179px) {
+    .sidebar-hidden .sidetoc {
+      display: none;
+    }
+  }
+
+  @media (max-width: 1439px) {
+    .sidebar-visible .sidetoc {
+      display: none;
+    }
+  }
+
+  @media (1180px <=width <=1439px) {
+    .sidebar-hidden main {
+      position: relative;
+      left: var(--center-content-toc-shift);
+    }
+  }
+
+  @media (1440px <=width <=1700px) {
+    .sidebar-visible main {
+      position: relative;
+      left: var(--center-content-toc-shift);
+    }
+  }
+
+  .content-wrap {
+    overflow-y: auto;
+    width: 100%;
+  }
+
+  .sidetoc {
+    margin-top: 20px;
+    margin-left: 10px;
+    margin-right: auto;
+  }
+
+  .pagetoc {
+    position: fixed;
+    /* adjust TOC width */
+    width: var(--toc-width);
+    height: calc(100vh - var(--menu-bar-height) - 0.67em * 4);
+    overflow: auto;
+  }
+
+  .pagetoc a {
+    border-left: 1px solid var(--sidebar-bg);
+    color: var(--fg) !important;
+    display: block;
+    padding-bottom: 5px;
+    padding-top: 5px;
+    padding-left: 10px;
+    text-align: left;
+    text-decoration: none;
+  }
+
+  .pagetoc a:hover,
+  .pagetoc a.active {
+    background: var(--sidebar-bg);
+    color: var(--sidebar-fg) !important;
+  }
+
+  .pagetoc .active {
+    background: var(--sidebar-bg);
+    color: var(--sidebar-fg);
+  }
+
+  .pagetoc .pagetoc-H2 {
+    padding-left: 20px;
+  }
+
+  .pagetoc .pagetoc-H3 {
+    padding-left: 40px;
+  }
+
+  .pagetoc .pagetoc-H4 {
+    padding-left: 60px;
+  }
+}
+
+@media screen and (max-width: 769px),
+print {
+  .sidetoc {
+    display: none;
+  }
+}

assets/pagetoc.js

@@ -0,0 +1,127 @@
+/** クライアントの環境がPCかどうか判定する */
+function isDesktop() {
+  const userAgent = navigator.userAgent;
+  const mobileRegex =
+    /Android|webOS|iPhone|iPad|iPod|BlackBerry|IEMobile|Opera Mini/i;
+  return !mobileRegex.test(userAgent);
+}
+
+/** 本体の処理 */
+function pageToc() {
+  function forEach(elems, fun) {
+    Array.prototype.forEach.call(elems, fun);
+  }
+
+  function getPagetoc() {
+    return document.getElementsByClassName("pagetoc")[0];
+  }
+
+  function getPagetocElems() {
+    return getPagetoc().children;
+  }
+
+  function getHeaders() {
+    return document.getElementsByClassName("header");
+  }
+
+  // Un-active everything when you click it
+  function forPagetocElem(fun) {
+    forEach(getPagetocElems(), fun);
+  }
+
+  function getRect(element) {
+    return element.getBoundingClientRect();
+  }
+
+  function overflowTop(container, element) {
+    return getRect(container).top - getRect(element).top;
+  }
+
+  function overflowBottom(container, element) {
+    return getRect(container).bottom - getRect(element).bottom;
+  }
+
+  let activeHref = location.href;
+
+  const updateFunction = (elem = undefined) => {
+    let id = elem;
+
+    if (!id && location.href !== activeHref) {
+      activeHref = location.href;
+      forPagetocElem((el) => {
+        if (el.href === activeHref) {
+          id = el;
+        }
+      });
+    }
+
+    if (!id) {
+      const elements = getHeaders();
+      const margin = window.innerHeight / 3;
+
+      forEach(elements, (el, i, arr) => {
+        if (!id && getRect(el).top >= 0) {
+          if (getRect(el).top < margin) {
+            id = el;
+          } else {
+            id = arr[Math.max(0, i - 1)];
+          }
+        }
+        // a very long last section
+        // its heading is over the screen
+        if (!id && i === arr.length - 1) {
+          id = el;
+        }
+      });
+    }
+
+    forPagetocElem((el) => {
+      el.classList.remove("active");
+    });
+
+    if (!id) return;
+
+    forPagetocElem((el) => {
+      if (id.href.localeCompare(el.href) === 0) {
+        el.classList.add("active");
+        const pagetoc = getPagetoc();
+        if (overflowTop(pagetoc, el) > 0) {
+          pagetoc.scrollTop = el.offsetTop;
+        }
+        if (overflowBottom(pagetoc, el) < 0) {
+          pagetoc.scrollTop -= overflowBottom(pagetoc, el);
+        }
+      }
+    });
+  };
+
+  const elements = getHeaders();
+
+  if (elements.length > 2) {
+    // Populate sidebar on load
+    window.addEventListener("load", () => {
+      const pagetoc = getPagetoc();
+      const elements = getHeaders();
+      forEach(elements, (el) => {
+        const link = document.createElement("a");
+        link.appendChild(document.createTextNode(el.text));
+        link.href = el.hash;
+        link.classList.add(`pagetoc-${el.parentElement.tagName}`);
+        pagetoc.appendChild(link);
+        link.onclick = () => {
+          updateFunction(link);
+        };
+      });
+      updateFunction();
+    });
+
+    // Handle active elements on scroll
+    window.addEventListener("scroll", () => {
+      updateFunction();
+    });
+  } else {
+    document.getElementsByClassName("sidetoc")[0].remove();
+  }
+}
+
+pageToc();

book.toml

@@ -6,4 +6,16 @@ src = "md"
 title = "Metaprogramming in Lean 4"
 
 [output.html]
-git-repository-url = "https://github.com/leanprover-community/lean4-metaprogramming-book"
+git-repository-url = "https://github.com/leanprover-community/lean4-metaprogramming-book"
+additional-css = ["./assets/pagetoc.css"]
+additional-js = [
+  "assets/blockPlay.js",
+  "assets/filePlay.js",
+  "assets/pagetoc.js",
+]
+
+# Settings to overwrite the edit button and make it a code execution button.
+edit-url-template = "https://raw.githubusercontent.com/leanprover-community/lean4-metaprogramming-book/master/{path}"
+
+# To ensure that the 404 page functions properly.
+site-url = "https://leanprover-community.github.io/lean4-metaprogramming-book/"

lake-manifest.json

@@ -15,11 +15,21 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
+   "rev": "194c47fd196790e6baa44cdbdf3b1babe59214b9",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v1.3.0",
+   "inputRev": "1.9.0",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c53b3371dd0fe5f3dd75a2df543c3550e246465a",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "«lean4-metaprogramming-book»",
  "lakeDir": ".lake"}

lakefile.lean

@@ -10,7 +10,7 @@ lean_lib «lean4-metaprogramming-book» where
   globs := #[Glob.one `cover, Glob.submodules `extra, Glob.submodules `main, Glob.submodules `solutions]
 
 require mdgen from git
-  "https://github.com/Seasawher/mdgen" @ "v1.3.0"
+  "https://github.com/Seasawher/mdgen" @ "1.9.0"
 
 require "leanprover-community" / "batteries" @ git "main"