diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 909c3b24..c23e68f9 100644 --- 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 index 23a61bff..40f246a2 100644 --- 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 index db54d0be..2db6bc99 100644 --- 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 index 4bcf09b6..a56c9fdb 100644 --- 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 index 276eb125..b810c80b 100644 --- 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,12 +43,12 @@ 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; } @@ -57,10 +56,10 @@ function pageToc() { } 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,20 +95,20 @@ 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); }; }); @@ -117,7 +116,7 @@ function pageToc() { }); // Handle active elements on scroll - window.addEventListener("scroll", function () { + window.addEventListener("scroll", () => { updateFunction(); }); } else { diff --git a/biome.json b/biome.json new file mode 100644 index 00000000..5d4a88ff --- /dev/null +++ b/biome.json @@ -0,0 +1,5 @@ +{ + "formatter": { + "indentStyle": "space" + } +}