Skip to content

Commit

Permalink
fix: always default ToC to closed on mobile
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Nov 19, 2024
1 parent 88d83d4 commit 6923069
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/verso-manual/VersoManual/Html/Style.lean
Original file line number Diff line number Diff line change
Expand Up @@ -626,11 +626,17 @@ def pageStyleJs : String := r####"
function saveCheckboxesInit() {
for (checkbox of document.querySelectorAll('#toc input[type="checkbox"]')) {
const value = localStorage.getItem(checkbox.id);
if (value === "true") {
// Treat the ToC toggle specially, because it should always default to
// closed on mobile-width screens but respect user preference on desktop-width.
if (checkbox.id === "toggle-toc" && window.matchMedia("(max-width: 700px)").matches) {
checkbox.checked = false;
} else if (value === "true") {
checkbox.checked = true;
} else if (value === "false") {
checkbox.checked = false;
} // if not found, do nothing
checkbox.addEventListener("change", persistCheckbox);
}
}
Expand Down

0 comments on commit 6923069

Please sign in to comment.