1"use strict"; 2 3const GLOSSARY_PAGE = "glossary.html"; 4 5const glossary_search = async () => { 6 const response = await fetch("_static/glossary.json"); 7 if (!response.ok) { 8 throw new Error("Failed to fetch glossary.json"); 9 } 10 const glossary = await response.json(); 11 12 const params = new URLSearchParams(document.location.search).get("q"); 13 if (!params) { 14 return; 15 } 16 17 const searchParam = params.toLowerCase(); 18 const glossaryItem = glossary[searchParam]; 19 if (!glossaryItem) { 20 return; 21 } 22 23 // set up the title text with a link to the glossary page 24 const glossaryTitle = document.getElementById("glossary-title"); 25 glossaryTitle.textContent = "Glossary: " + glossaryItem.title; 26 const linkTarget = searchParam.replace(/ /g, "-"); 27 glossaryTitle.href = GLOSSARY_PAGE + "#term-" + linkTarget; 28 29 // rewrite any anchor links (to other glossary terms) 30 // to have a full reference to the glossary page 31 const glossaryBody = document.getElementById("glossary-body"); 32 glossaryBody.innerHTML = glossaryItem.body; 33 const anchorLinks = glossaryBody.querySelectorAll('a[href^="#"]'); 34 anchorLinks.forEach(function (link) { 35 const currentUrl = link.getAttribute("href"); 36 link.href = GLOSSARY_PAGE + currentUrl; 37 }); 38 39 const glossaryResult = document.getElementById("glossary-result"); 40 glossaryResult.style.display = ""; 41}; 42 43if (document.readyState !== "loading") { 44 glossary_search().catch(console.error); 45} else { 46 document.addEventListener("DOMContentLoaded", glossary_search); 47} 48