Skip to content

Commit 5498cd3

Browse files
robsimmonsrobsimmons
committed
refactor: configurable source for highlighting
1 parent 113c54a commit 5498cd3

1 file changed

Lines changed: 154 additions & 146 deletions

File tree

‎src/verso/Verso/Code/Highlighted.lean‎

Lines changed: 154 additions & 146 deletions
Original file line numberDiff line numberDiff line change
@@ -1354,9 +1354,19 @@ Some CSS frameworks customize details/summary in ways not compatible with Verso'
13541354
13551355
"
13561356

1357-
public def highlightingJs : String :=
1357+
/--
1358+
fetch highlighting data from `-verso-docs.json` (default behavior)
1359+
-/
1360+
public def fetchDocsJson : String :=
1361+
"fetch(\"-verso-docs.json\").then((resp) => resp.json())"
1362+
1363+
/--
1364+
Given an await-able JavaScript expression for obtaining highlighting data,
1365+
render highlights and hovers.
1366+
-/
1367+
public def highlightingJs (highlightJson : String := fetchDocsJson) : String :=
13581368
"
1359-
window.onload = () => {
1369+
window.onload = async () => {
13601370
13611371
// Don't show hovers inside of closed tactic states
13621372
function blockedByTactic(elem) {
@@ -1430,164 +1440,162 @@ window.onload = () => {
14301440
}
14311441
}
14321442
// Add hovers
1433-
let docsJson = \"-verso-docs.json\";
1434-
fetch(docsJson).then((resp) => resp.json()).then((versoDocData) => {
1435-
1436-
function hideParentTooltips(element) {
1437-
let parent = element.parentElement;
1438-
while (parent) {
1439-
const tippyInstance = parent._tippy;
1440-
if (tippyInstance) {
1441-
tippyInstance.hide();
1442-
}
1443-
parent = parent.parentElement;
1443+
const versoDocData = await " ++ highlightJson ++ "
1444+
1445+
function hideParentTooltips(element) {
1446+
let parent = element.parentElement;
1447+
while (parent) {
1448+
const tippyInstance = parent._tippy;
1449+
if (tippyInstance) {
1450+
tippyInstance.hide();
14441451
}
1452+
parent = parent.parentElement;
14451453
}
1454+
}
14461455
14471456
14481457
1449-
const defaultTippyProps = {
1450-
/* DEBUG -- remove the space: * /
1451-
onHide(any) { return false; },
1452-
trigger: \"click\",
1453-
// */
1454-
/* theme: \"lean\", */
1455-
maxWidth: \"none\",
1456-
appendTo: () => document.body,
1457-
interactive: true,
1458-
delay: [100, null],
1459-
/* ignoreAttributes: true, */
1460-
followCursor: 'initial',
1461-
onShow(inst) {
1462-
if (inst.reference.className == 'tactic') {
1463-
const toggle = inst.reference.querySelector(\":scope > input.tactic-toggle\");
1464-
if (toggle && toggle.checked) {
1465-
return false;
1466-
}
1467-
hideParentTooltips(inst.reference);
1468-
if (blockedByTippy(inst.reference)) { return false; }
1469-
1470-
} else if (inst.reference.querySelector(\".hover-info\") || \"versoHover\" in inst.reference.dataset) {
1471-
if (blockedByTactic(inst.reference)) { return false };
1472-
if (blockedByTippy(inst.reference)) { return false; }
1473-
} else { // Nothing to show here!
1458+
const defaultTippyProps = {
1459+
/* DEBUG -- remove the space: * /
1460+
onHide(any) { return false; },
1461+
trigger: \"click\",
1462+
// */
1463+
/* theme: \"lean\", */
1464+
maxWidth: \"none\",
1465+
appendTo: () => document.body,
1466+
interactive: true,
1467+
delay: [100, null],
1468+
/* ignoreAttributes: true, */
1469+
followCursor: 'initial',
1470+
onShow(inst) {
1471+
if (inst.reference.className == 'tactic') {
1472+
const toggle = inst.reference.querySelector(\":scope > input.tactic-toggle\");
1473+
if (toggle && toggle.checked) {
14741474
return false;
14751475
}
1476-
},
1477-
onShown(inst) { visibleTippyCount++; },
1478-
onHidden(inst) { visibleTippyCount = Math.max(0, visibleTippyCount - 1); },
1479-
content (tgt) {
1480-
const content = document.createElement(\"span\");
1481-
if (tgt.className == 'tactic') {
1482-
const state = tgt.querySelector(\":scope > .tactic-state\").cloneNode(true);
1483-
state.style.display = \"block\";
1484-
content.appendChild(state);
1485-
content.style.display = \"block\";
1486-
content.className = \"hl lean popup\";
1487-
} else {
1488-
content.className = \"hl lean\";
1489-
content.style.display = \"block\";
1490-
content.style.maxHeight = \"300px\";
1491-
content.style.overflowY = \"auto\";
1492-
content.style.overflowX = \"hidden\";
1493-
const hoverId = tgt.dataset.versoHover;
1494-
const hoverInfo = tgt.querySelector(\".hover-info\");
1495-
if (hoverId) { // Docstrings from the table
1496-
// TODO stop doing an implicit conversion from string to number here
1497-
let data = versoDocData[hoverId];
1498-
if (data) {
1499-
const info = document.createElement(\"span\");
1500-
info.className = \"hover-info\";
1501-
info.style.display = \"block\";
1502-
info.innerHTML = data;
1503-
content.appendChild(info);
1504-
/* Render docstrings - TODO server-side */
1505-
if ('undefined' !== typeof marked) {
1506-
for (const d of content.querySelectorAll(\"code.docstring, pre.docstring\")) {
1507-
const str = d.innerText;
1508-
const html = marked.parse(str);
1509-
const rendered = document.createElement(\"div\");
1510-
rendered.classList.add(\"docstring\");
1511-
rendered.innerHTML = html;
1512-
d.parentNode.replaceChild(rendered, d);
1513-
}
1514-
}
1515-
} else {
1516-
content.innerHTML = \"Failed to load doc ID: \" + hoverId;
1476+
hideParentTooltips(inst.reference);
1477+
if (blockedByTippy(inst.reference)) { return false; }
1478+
1479+
} else if (inst.reference.querySelector(\".hover-info\") || \"versoHover\" in inst.reference.dataset) {
1480+
if (blockedByTactic(inst.reference)) { return false };
1481+
if (blockedByTippy(inst.reference)) { return false; }
1482+
} else { // Nothing to show here!
1483+
return false;
1484+
}
1485+
},
1486+
onShown(inst) { visibleTippyCount++; },
1487+
onHidden(inst) { visibleTippyCount = Math.max(0, visibleTippyCount - 1); },
1488+
content (tgt) {
1489+
const content = document.createElement(\"span\");
1490+
if (tgt.className == 'tactic') {
1491+
const state = tgt.querySelector(\":scope > .tactic-state\").cloneNode(true);
1492+
state.style.display = \"block\";
1493+
content.appendChild(state);
1494+
content.style.display = \"block\";
1495+
content.className = \"hl lean popup\";
1496+
} else {
1497+
content.className = \"hl lean\";
1498+
content.style.display = \"block\";
1499+
content.style.maxHeight = \"300px\";
1500+
content.style.overflowY = \"auto\";
1501+
content.style.overflowX = \"hidden\";
1502+
const hoverId = tgt.dataset.versoHover;
1503+
const hoverInfo = tgt.querySelector(\".hover-info\");
1504+
if (hoverId) { // Docstrings from the table
1505+
// TODO stop doing an implicit conversion from string to number here
1506+
let data = versoDocData[hoverId];
1507+
if (data) {
1508+
const info = document.createElement(\"span\");
1509+
info.className = \"hover-info\";
1510+
info.style.display = \"block\";
1511+
info.innerHTML = data;
1512+
content.appendChild(info);
1513+
/* Render docstrings - TODO server-side */
1514+
if ('undefined' !== typeof marked) {
1515+
for (const d of content.querySelectorAll(\"code.docstring, pre.docstring\")) {
1516+
const str = d.innerText;
1517+
const html = marked.parse(str);
1518+
const rendered = document.createElement(\"div\");
1519+
rendered.classList.add(\"docstring\");
1520+
rendered.innerHTML = html;
1521+
d.parentNode.replaceChild(rendered, d);
1522+
}
15171523
}
1518-
} else if (hoverInfo) { // The inline info, still used for compiler messages
1519-
content.appendChild(hoverInfo.cloneNode(true));
1524+
} else {
1525+
content.innerHTML = \"Failed to load doc ID: \" + hoverId;
15201526
}
1521-
const extraLinks = tgt.parentElement.dataset['versoLinks'];
1522-
if (extraLinks) {
1523-
try {
1524-
const extras = JSON.parse(extraLinks);
1525-
const links = document.createElement('ul');
1526-
links.className = 'extra-doc-links';
1527-
extras.forEach((l) => {
1528-
const li = document.createElement('li');
1529-
li.innerHTML = \"<a href=\\\"\" + l['href'] + \"\\\" title=\\\"\" + l.long + \"\\\">\" + l.short + \"</a>\";
1530-
links.appendChild(li);
1531-
});
1532-
content.appendChild(links);
1533-
} catch (error) {
1534-
console.error(error);
1535-
}
1527+
} else if (hoverInfo) { // The inline info, still used for compiler messages
1528+
content.appendChild(hoverInfo.cloneNode(true));
1529+
}
1530+
const extraLinks = tgt.parentElement.dataset['versoLinks'];
1531+
if (extraLinks) {
1532+
try {
1533+
const extras = JSON.parse(extraLinks);
1534+
const links = document.createElement('ul');
1535+
links.className = 'extra-doc-links';
1536+
extras.forEach((l) => {
1537+
const li = document.createElement('li');
1538+
li.innerHTML = \"<a href=\\\"\" + l['href'] + \"\\\" title=\\\"\" + l.long + \"\\\">\" + l.short + \"</a>\";
1539+
links.appendChild(li);
1540+
});
1541+
content.appendChild(links);
1542+
} catch (error) {
1543+
console.error(error);
15361544
}
15371545
}
1538-
return content;
15391546
}
1540-
};
1541-
1542-
1543-
document.querySelectorAll('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort').forEach(element => {
1544-
element.setAttribute('data-tippy-theme', 'lean');
1545-
});
1546-
document.querySelectorAll('.hl.lean .has-info.warning').forEach(element => {
1547-
element.setAttribute('data-tippy-theme', 'warning message');
1548-
});
1549-
document.querySelectorAll('.hl.lean .has-info.information').forEach(element => {
1550-
element.setAttribute('data-tippy-theme', 'info message');
1551-
});
1552-
document.querySelectorAll('.hl.lean .has-info.error').forEach(element => {
1553-
element.setAttribute('data-tippy-theme', 'error message');
1554-
});
1555-
document.querySelectorAll('.hl.lean .tactic').forEach(element => {
1556-
element.setAttribute('data-tippy-theme', 'tactic');
1557-
});
1558-
// Skip tokens inside closed tactics — they interfere with tactic tippys
1559-
const closedTactics = new Set();
1560-
document.querySelectorAll('.hl.lean .tactic').forEach(tactic => {
1561-
const toggle = tactic.querySelector(':scope > input.tactic-toggle');
1562-
if (toggle && !toggle.checked) closedTactics.add(tactic);
1563-
});
1564-
function isInsideClosedTactic(el) {
1565-
const tactic = el.closest('.tactic');
1566-
return tactic && tactic !== el && closedTactics.has(tactic);
1547+
return content;
15671548
}
1549+
};
1550+
1551+
1552+
document.querySelectorAll('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort').forEach(element => {
1553+
element.setAttribute('data-tippy-theme', 'lean');
1554+
});
1555+
document.querySelectorAll('.hl.lean .has-info.warning').forEach(element => {
1556+
element.setAttribute('data-tippy-theme', 'warning message');
1557+
});
1558+
document.querySelectorAll('.hl.lean .has-info.information').forEach(element => {
1559+
element.setAttribute('data-tippy-theme', 'info message');
1560+
});
1561+
document.querySelectorAll('.hl.lean .has-info.error').forEach(element => {
1562+
element.setAttribute('data-tippy-theme', 'error message');
1563+
});
1564+
document.querySelectorAll('.hl.lean .tactic').forEach(element => {
1565+
element.setAttribute('data-tippy-theme', 'tactic');
1566+
});
1567+
// Skip tokens inside closed tactics — they interfere with tactic tippys
1568+
const closedTactics = new Set();
1569+
document.querySelectorAll('.hl.lean .tactic').forEach(tactic => {
1570+
const toggle = tactic.querySelector(':scope > input.tactic-toggle');
1571+
if (toggle && !toggle.checked) closedTactics.add(tactic);
1572+
});
1573+
function isInsideClosedTactic(el) {
1574+
const tactic = el.closest('.tactic');
1575+
return tactic && tactic !== el && closedTactics.has(tactic);
1576+
}
15681577
1569-
const tokenSelector = '.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .has-info, .hl.lean .tactic, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort';
1570-
tippy(Array.from(document.querySelectorAll(tokenSelector)).filter(el => !isInsideClosedTactic(el)), defaultTippyProps);
1571-
1572-
// Create/destroy token tippys when tactic checkbox toggles
1573-
const tacticTippySelector = '.const.token, .keyword.token, .literal.token, .option.token, .var.token, .typed.token, .has-info, .level-var, .level-const, .level-op, .sort';
1574-
document.querySelectorAll('.hl.lean .tactic').forEach(tactic => {
1575-
const toggle = tactic.querySelector(':scope > input.tactic-toggle');
1576-
if (toggle) toggle.addEventListener('change', () => {
1577-
if (toggle.checked) {
1578-
closedTactics.delete(tactic);
1579-
tactic.querySelectorAll('.token').forEach(tok => {
1580-
if (!tok._tippy && tok.matches(tacticTippySelector)) {
1581-
tippy(tok, defaultTippyProps);
1582-
}
1583-
});
1584-
} else {
1585-
closedTactics.add(tactic);
1586-
tactic.querySelectorAll('.token').forEach(tok => {
1587-
if (tok._tippy) tok._tippy.destroy();
1588-
});
1589-
}
1590-
});
1578+
const tokenSelector = '.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token, .hl.lean .typed.token, .hl.lean .has-info, .hl.lean .tactic, .hl.lean .level-var, .hl.lean .level-const, .hl.lean .level-op, .hl.lean .sort';
1579+
tippy(Array.from(document.querySelectorAll(tokenSelector)).filter(el => !isInsideClosedTactic(el)), defaultTippyProps);
1580+
1581+
// Create/destroy token tippys when tactic checkbox toggles
1582+
const tacticTippySelector = '.const.token, .keyword.token, .literal.token, .option.token, .var.token, .typed.token, .has-info, .level-var, .level-const, .level-op, .sort';
1583+
document.querySelectorAll('.hl.lean .tactic').forEach(tactic => {
1584+
const toggle = tactic.querySelector(':scope > input.tactic-toggle');
1585+
if (toggle) toggle.addEventListener('change', () => {
1586+
if (toggle.checked) {
1587+
closedTactics.delete(tactic);
1588+
tactic.querySelectorAll('.token').forEach(tok => {
1589+
if (!tok._tippy && tok.matches(tacticTippySelector)) {
1590+
tippy(tok, defaultTippyProps);
1591+
}
1592+
});
1593+
} else {
1594+
closedTactics.add(tactic);
1595+
tactic.querySelectorAll('.token').forEach(tok => {
1596+
if (tok._tippy) tok._tippy.destroy();
1597+
});
1598+
}
15911599
});
15921600
});
15931601
}

0 commit comments

Comments
 (0)