Merge pull request #868 from lean-ja/Seasawher/issue861

Biome で js ファイルのフォーマットなどを行う
lean-ja · Sep 22, 2024 · 1311998 · 1311998
2 parents fdf689d + d7201f1
commit 1311998
Show file tree

Hide file tree

Showing 6 changed files with 75 additions and 57 deletions.
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -25,7 +25,8 @@
         "usernamehw.errorlens",
         "piousdeer.horizon-theme-vscode-default-token-colors",
         "EditorConfig.EditorConfig",
-        "mfeckies.handlebars-formatter"
+        "mfeckies.handlebars-formatter",
+        "biomejs.biome"
       ]
     }
   }

diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -16,6 +16,12 @@
     "editor.rulers": [80],
   },
 
+  // javascript の設定
+  "[javascript]": {
+    "editor.defaultFormatter": "biomejs.biome",
+    "editor.formatOnSave": true,
+  },
+
   // Handlebars の設定
   "[handlebars]": {
     "editor.defaultFormatter": "mfeckies.handlebars-formatter",

diff --git a/assets/blockPlay.js b/assets/blockPlay.js
@@ -1,27 +1,31 @@
-"use strict";
-
-(function blockPlay() {
-  Array.from(document.querySelectorAll(".language-lean")).forEach(function (code_block) {
-    let pre_block = code_block.parentElement;
+/**
+ * lean4 のコードブロック内に、Lean 4 web playground へジャンプするボタンを追加する
+ */
+function blockPlay() {
+  const array = Array.from(document.querySelectorAll(".language-lean"));
+  for (const code_block of array) {
+    const pre_block = code_block.parentElement;
 
     // lean4 web editor へのリンクを生成する
-    let escaped_code = encodeURIComponent(code_block.textContent);
-    let url = `https://live.lean-lang.org/#code=${escaped_code}`;
+    const escaped_code = encodeURIComponent(code_block.textContent);
+    const url = `https://live.lean-lang.org/#code=${escaped_code}`;
 
     // ボタンを生成する
-    let buttons = pre_block.querySelector(".buttons");
-    let leanWebButton = document.createElement('button');
-    leanWebButton.className = 'fa fa-external-link lean-web-button';
+    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);
+    leanWebButton.title = "Run on lean4 playground";
+    leanWebButton.setAttribute("aria-label", leanWebButton.title);
 
     // ボタンを挿入する
     buttons.insertBefore(leanWebButton, buttons.firstChild);
 
     // ボタンをクリックしたときに、lean4 web editor を開く
-    leanWebButton.addEventListener('click', function (e) {
+    leanWebButton.addEventListener("click", (e) => {
       open(url);
     });
-  });
-})();
+  }
+}
+
+blockPlay();
diff --git a/assets/filePlay.js b/assets/filePlay.js
@@ -2,34 +2,37 @@
  * mdbook の "Suggest an edit" ボタンを改造し、
  * lean4 web editor へのリンクにしてしまう
  */
-"use strict";
-
-(function filePlay() {
+function filePlay() {
   // 編集ボタンのアイコン部分の `i` 要素
-  const editButtonIcon = document.querySelector('#git-edit-button');
-  editButtonIcon.className = 'fa fa-play';
-  editButtonIcon.id = 'lean-play-button';
+  const editButtonIcon = document.querySelector("#git-edit-button");
+  editButtonIcon.className = "fa fa-play";
+  editButtonIcon.id = "lean-play-button";
 
   // 編集ボタンを表す `a` 要素
   const editButtonLink = editButtonIcon.parentElement;
-  editButtonLink.title = 'Run on Lean 4 playground';
+  editButtonLink.title = "Run on Lean 4 playground";
   editButtonLink.ariaLabel = editButtonLink.title;
 
   // 拡張子が `.md` になっているので `.lean` に修正する
-  editButtonLink.href = editButtonLink.href.replace(/\.md$/, '.lean');
+  editButtonLink.href = editButtonLink.href.replace(/\.md$/, ".lean");
 
   // Lean ファイルがあるのは `src` ではなく `Examples` ディレクトリ
-  editButtonLink.href = editButtonLink.href.replace('/src/', '/Examples/');
+  editButtonLink.href = editButtonLink.href.replace("/src/", "/Examples/");
 
   // 演習問題のファイルのみ、`Examples` ディレクトリではなくて `Exercise` ディレクトリにある
-  editButtonLink.href = editButtonLink.href.replace('/Examples/Exercise/', '/Exercise/');
+  editButtonLink.href = editButtonLink.href.replace(
+    "/Examples/Exercise/",
+    "/Exercise/",
+  );
 
   // URL を書き換える
   fetch(editButtonLink.href)
-    .then(response => response.text())
-    .then(body => {
+    .then((response) => response.text())
+    .then((body) => {
       const escaped_code = encodeURIComponent(body);
       const url = `https://live.lean-lang.org/#code=${escaped_code}`;
       editButtonLink.href = url;
     });
-})();
+}
+
+filePlay();
diff --git a/assets/pagetoc.js b/assets/pagetoc.js
@@ -1,9 +1,8 @@
-"use strict";
-
 /** クライアントの環境がPCかどうか判定する */
 function isDesktop() {
   const userAgent = navigator.userAgent;
-  const mobileRegex = /Android|webOS|iPhone|iPad|iPod|BlackBerry|IEMobile|Opera Mini/i;
+  const mobileRegex =
+    /Android|webOS|iPhone|iPad|iPod|BlackBerry|IEMobile|Opera Mini/i;
   return !mobileRegex.test(userAgent);
 }
 
@@ -13,16 +12,16 @@ function pageToc() {
     Array.prototype.forEach.call(elems, fun);
   }
 
-  function getPagetoc(){
-    return document.getElementsByClassName("pagetoc")[0]
+  function getPagetoc() {
+    return document.getElementsByClassName("pagetoc")[0];
   }
 
   function getPagetocElems() {
     return getPagetoc().children;
   }
 
-  function getHeaders(){
-    return document.getElementsByClassName("header")
+  function getHeaders() {
+    return document.getElementsByClassName("header");
   }
 
   // Un-active everything when you click it
@@ -44,23 +43,23 @@ function pageToc() {
 
   let activeHref = location.href;
 
-  let updateFunction = function (elem = undefined) {
+  const updateFunction = (elem = undefined) => {
     let id = elem;
 
-    if (!id && location.href != activeHref) {
+    if (!id && location.href !== activeHref) {
       activeHref = location.href;
-      forPagetocElem(function (el) {
+      forPagetocElem((el) => {
         if (el.href === activeHref) {
           id = el;
         }
       });
     }
 
     if (!id) {
-      let elements = getHeaders();
-      let margin = window.innerHeight / 3;
+      const elements = getHeaders();
+      const margin = window.innerHeight / 3;
 
-      forEach(elements, function (el, i, arr) {
+      forEach(elements, (el, i, arr) => {
         if (!id && getRect(el).top >= 0) {
           if (getRect(el).top < margin) {
             id = el;
@@ -70,22 +69,22 @@ function pageToc() {
         }
         // a very long last section
         // its heading is over the screen
-        if (!id && i == arr.length - 1) {
-          id = el
+        if (!id && i === arr.length - 1) {
+          id = el;
         }
       });
     }
 
-    forPagetocElem(function (el) {
+    forPagetocElem((el) => {
       el.classList.remove("active");
     });
 
     if (!id) return;
 
-    forPagetocElem(function (el) {
-      if (id.href.localeCompare(el.href) == 0) {
+    forPagetocElem((el) => {
+      if (id.href.localeCompare(el.href) === 0) {
         el.classList.add("active");
-        let pagetoc = getPagetoc();
+        const pagetoc = getPagetoc();
         if (overflowTop(pagetoc, el) > 0) {
           pagetoc.scrollTop = el.offsetTop;
         }
@@ -96,28 +95,28 @@ function pageToc() {
     });
   };
 
-  let elements = getHeaders();
+  const elements = getHeaders();
 
   if (elements.length > 2) {
     // Populate sidebar on load
-    window.addEventListener("load", function () {
-      let pagetoc = getPagetoc();
-      let elements = getHeaders();
-      forEach(elements, function (el) {
-        let link = document.createElement("a");
+    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);
+        link.classList.add(`pagetoc-${el.parentElement.tagName}`);
         pagetoc.appendChild(link);
-        link.onclick = function () {
+        link.onclick = () => {
           updateFunction(link);
         };
       });
       updateFunction();
     });
 
     // Handle active elements on scroll
-    window.addEventListener("scroll", function () {
+    window.addEventListener("scroll", () => {
       updateFunction();
     });
   } else {

diff --git a/biome.json b/biome.json
@@ -0,0 +1,5 @@
+{
+  "formatter": {
+    "indentStyle": "space"
+  }
+}