feat: import nav.js
Just a copy and paste + include in the template, it will most likely have to be modified in the future.main
parent
ef8ecec0d7
commit
551eeee09d
|
@ -125,8 +125,14 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do
|
|||
{site}
|
||||
|
||||
{←navbar}
|
||||
-- TODO Add the js stuff
|
||||
|
||||
-- Lean in JS in HTML in Lean...very meta
|
||||
<script>
|
||||
siteRoot = "{←getRoot}";
|
||||
</script>
|
||||
|
||||
-- TODO Add more js stuff
|
||||
<script src={s!"{←getRoot}nav.js"}></script>
|
||||
</body>
|
||||
</html>
|
||||
|
||||
|
@ -145,6 +151,7 @@ def index : HtmlM Html := do templateExtends (baseHtml "Index") $
|
|||
</main>
|
||||
|
||||
def styleCss : String := include_str "./static/style.css"
|
||||
def navJs : String := include_str "./static/nav.js"
|
||||
|
||||
def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
|
||||
templateExtends (baseHtml module.name.toString) $
|
||||
|
@ -162,6 +169,7 @@ def htmlOutput (result : AnalyzerResult) : IO Unit := do
|
|||
FS.writeFile (basePath / "index.html") indexHtml.toString
|
||||
FS.writeFile (basePath / "style.css") styleCss
|
||||
FS.writeFile (basePath / "404.html") notFoundHtml.toString
|
||||
FS.writeFile (basePath / "nav.js") navJs
|
||||
for (module, content) in result.modules.toArray do
|
||||
let moduleHtml := ReaderT.run (moduleToHtml content) config
|
||||
let path := basePath / (nameToUrl module)
|
||||
|
|
|
@ -0,0 +1,239 @@
|
|||
// Persistent expansion cookie for the file tree
|
||||
// ---------------------------------------------
|
||||
|
||||
let expanded = {};
|
||||
for (const e of (sessionStorage.getItem('expanded') || '').split(',')) {
|
||||
if (e !== '') {
|
||||
expanded[e] = true;
|
||||
}
|
||||
}
|
||||
|
||||
function saveExpanded() {
|
||||
sessionStorage.setItem("expanded",
|
||||
Object.getOwnPropertyNames(expanded).filter((e) => expanded[e]).join(","));
|
||||
}
|
||||
|
||||
for (const elem of document.getElementsByClassName('nav_sect')) {
|
||||
const id = elem.getAttribute('data-path');
|
||||
if (!id) continue;
|
||||
if (expanded[id]) {
|
||||
elem.open = true;
|
||||
}
|
||||
elem.addEventListener('toggle', () => {
|
||||
expanded[id] = elem.open;
|
||||
saveExpanded();
|
||||
});
|
||||
}
|
||||
|
||||
for (const currentFileLink of document.getElementsByClassName('visible')) {
|
||||
currentFileLink.scrollIntoView({block: 'center'});
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
// Tactic list tag filter
|
||||
// ----------------------
|
||||
|
||||
function filterSelectionClass(tagNames, classname) {
|
||||
if (tagNames.length == 0) {
|
||||
for (const elem of document.getElementsByClassName(classname)) {
|
||||
elem.classList.remove("hide");
|
||||
}
|
||||
} else {
|
||||
// Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
|
||||
for (const elem of document.getElementsByClassName(classname)) {
|
||||
elem.classList.add("hide");
|
||||
for (const tagName of tagNames) {
|
||||
if (elem.classList.contains(tagName)) {
|
||||
elem.classList.remove("hide");
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
function filterSelection(c) {
|
||||
filterSelectionClass(c, "tactic");
|
||||
filterSelectionClass(c, "taclink");
|
||||
}
|
||||
|
||||
var filterBoxes = document.getElementsByClassName("tagfilter");
|
||||
|
||||
function updateDisplay() {
|
||||
filterSelection(getSelectValues());
|
||||
}
|
||||
|
||||
function getSelectValues() {
|
||||
var result = [];
|
||||
|
||||
for (const opt of filterBoxes) {
|
||||
|
||||
if (opt.checked) {
|
||||
result.push(opt.value);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
function setSelectVal(val) {
|
||||
for (const opt of filterBoxes) {
|
||||
opt.checked = val;
|
||||
}
|
||||
}
|
||||
|
||||
updateDisplay();
|
||||
|
||||
for (const opt of filterBoxes) {
|
||||
opt.addEventListener('change', updateDisplay);
|
||||
}
|
||||
|
||||
const tse = document.getElementById("tagfilter-selectall")
|
||||
if (tse != null) {
|
||||
tse.addEventListener('change', function() {
|
||||
setSelectVal(this.checked);
|
||||
updateDisplay();
|
||||
});
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
// Simple declaration search
|
||||
// -------------------------
|
||||
|
||||
const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location);
|
||||
const declSearch = (q) => new Promise((resolve, reject) => {
|
||||
const worker = new SharedWorker(searchWorkerURL);
|
||||
worker.port.start();
|
||||
worker.port.onmessage = ({data}) => resolve(data);
|
||||
worker.port.onmessageerror = (e) => reject(e);
|
||||
worker.port.postMessage({q});
|
||||
});
|
||||
|
||||
const srId = 'search_results';
|
||||
document.getElementById('search_form')
|
||||
.appendChild(document.createElement('div'))
|
||||
.id = srId;
|
||||
|
||||
function handleSearchCursorUpDown(down) {
|
||||
const sel = document.querySelector(`#${srId} .selected`);
|
||||
const sr = document.getElementById(srId);
|
||||
if (sel) {
|
||||
sel.classList.remove('selected');
|
||||
const toSelect = down ?
|
||||
sel.nextSibling || sr.firstChild:
|
||||
sel.previousSibling || sr.lastChild;
|
||||
toSelect && toSelect.classList.add('selected');
|
||||
} else {
|
||||
const toSelect = down ? sr.firstChild : sr.lastChild;
|
||||
toSelect && toSelect.classList.add('selected');
|
||||
}
|
||||
}
|
||||
|
||||
function handleSearchEnter() {
|
||||
const sel = document.querySelector(`#${srId} .selected`)
|
||||
|| document.getElementById(srId).firstChild;
|
||||
sel.click();
|
||||
}
|
||||
|
||||
const searchInput = document.querySelector('#search_form input[name=q]');
|
||||
|
||||
searchInput.addEventListener('keydown', (ev) => {
|
||||
switch (ev.key) {
|
||||
case 'Down':
|
||||
case 'ArrowDown':
|
||||
ev.preventDefault();
|
||||
handleSearchCursorUpDown(true);
|
||||
break;
|
||||
case 'Up':
|
||||
case 'ArrowUp':
|
||||
ev.preventDefault();
|
||||
handleSearchCursorUpDown(false);
|
||||
break;
|
||||
case 'Enter':
|
||||
ev.preventDefault();
|
||||
handleSearchEnter();
|
||||
break;
|
||||
}
|
||||
});
|
||||
|
||||
searchInput.addEventListener('input', async (ev) => {
|
||||
const text = ev.target.value;
|
||||
|
||||
if (!text) {
|
||||
const sr = document.getElementById(srId);
|
||||
sr.removeAttribute('state');
|
||||
sr.replaceWith(sr.cloneNode(false));
|
||||
return;
|
||||
}
|
||||
|
||||
document.getElementById(srId).setAttribute('state', 'loading');
|
||||
|
||||
const result = await declSearch(text);
|
||||
if (ev.target.value != text) return;
|
||||
|
||||
const oldSR = document.getElementById('search_results');
|
||||
const sr = oldSR.cloneNode(false);
|
||||
for (const {decl} of result) {
|
||||
const d = sr.appendChild(document.createElement('a'));
|
||||
d.innerText = decl;
|
||||
d.title = decl;
|
||||
d.href = `${siteRoot}find/${decl}`;
|
||||
}
|
||||
sr.setAttribute('state', 'done');
|
||||
oldSR.replaceWith(sr);
|
||||
});
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
// 404 page goodies
|
||||
// ----------------
|
||||
|
||||
const howabout = document.getElementById('howabout');
|
||||
if (howabout) {
|
||||
howabout.innerText = "Please wait a second. I'll try to help you.";
|
||||
|
||||
howabout.parentNode
|
||||
.insertBefore(document.createElement('pre'), howabout)
|
||||
.appendChild(document.createElement('code'))
|
||||
.innerText = window.location.href.replace(/[/]/g, '/\u200b');
|
||||
|
||||
const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1];
|
||||
declSearch(query).then((results) => {
|
||||
howabout.innerText = 'How about one of these instead:';
|
||||
const ul = howabout.appendChild(document.createElement('ul'));
|
||||
for (const {decl} of results) {
|
||||
const li = ul.appendChild(document.createElement('li'));
|
||||
const a = li.appendChild(document.createElement('a'));
|
||||
a.href = `${siteRoot}find/${decl}`;
|
||||
a.appendChild(document.createElement('code')).innerText = decl;
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
// Rewrite GitHub links
|
||||
// --------------------
|
||||
|
||||
for (const elem of document.getElementsByClassName('gh_link')) {
|
||||
const a = elem.firstElementChild;
|
||||
// commit is set in add_commit.js
|
||||
for (const [prefix, replacement] of commit) {
|
||||
if (a.href.startsWith(prefix)) {
|
||||
a.href = a.href.replace(prefix, replacement);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue