| |
| (() => { |
| const body = document.body; |
|
|
| |
| const copyLabel = body.dataset.copy || "Copy"; |
| const copiedLabel = body.dataset.copied || "Copied"; |
| const copyText = async (text) => { |
| try { |
| await navigator.clipboard.writeText(text); |
| return true; |
| } catch (err) { |
| const area = document.createElement("textarea"); |
| area.value = text; |
| area.setAttribute("readonly", ""); |
| area.style.position = "fixed"; |
| area.style.opacity = "0"; |
| document.body.append(area); |
| area.select(); |
| let ok = false; |
| try { |
| ok = document.execCommand("copy"); |
| } catch (e) { |
| ok = false; |
| } |
| area.remove(); |
| return ok; |
| } |
| }; |
| document.querySelectorAll(".code").forEach((block) => { |
| const head = block.querySelector(".code-head"); |
| const pre = block.querySelector("pre"); |
| if (!head || !pre) return; |
| const button = document.createElement("button"); |
| button.type = "button"; |
| button.className = "copy"; |
| button.textContent = copyLabel; |
| button.addEventListener("click", async () => { |
| if (!(await copyText(pre.innerText.replace(/\n$/, "")))) return; |
| button.textContent = copiedLabel; |
| button.classList.add("done"); |
| clearTimeout(button.copyTimer); |
| button.copyTimer = setTimeout(() => { |
| button.textContent = copyLabel; |
| button.classList.remove("done"); |
| }, 1600); |
| }); |
| head.append(button); |
| }); |
|
|
| |
| const links = [...document.querySelectorAll(".toc a[href^='#']")]; |
| if (!links.length) return; |
| const byId = new Map(links.map((a) => [decodeURIComponent(a.hash.slice(1)), a])); |
| const heads = [...document.querySelectorAll(".prose :is(h1, h2, h3)[id]")].filter((h) => byId.has(h.id)); |
| let current = null; |
| let queued = false; |
| const mark = () => { |
| queued = false; |
| const line = 120; |
| let found = heads[0]; |
| for (const h of heads) { |
| if (h.getBoundingClientRect().top <= line) found = h; |
| else break; |
| } |
| const link = found ? byId.get(found.id) : null; |
| if (link === current) return; |
| if (current) current.removeAttribute("aria-current"); |
| current = link; |
| if (current) { |
| current.setAttribute("aria-current", "location"); |
| const toc = current.closest(".toc"); |
| if (toc) { |
| const top = current.offsetTop - toc.scrollTop; |
| if (top < 0 || top > toc.clientHeight - current.offsetHeight) { |
| toc.scrollTop = current.offsetTop - toc.clientHeight / 3; |
| } |
| } |
| } |
| }; |
| window.addEventListener("scroll", () => { |
| if (!queued) { |
| queued = true; |
| requestAnimationFrame(mark); |
| } |
| }, { passive: true }); |
| mark(); |
| })(); |
|
|
