feat: expand the current file in the navbar

main
Alex J. Best 2023-09-18 22:03:40 +01:00 committed by Henrik Böving
parent 34185d4fef
commit 924be4c7d8
6 changed files with 22 additions and 0 deletions

View File

@ -42,6 +42,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
("declaration-data.js", declarationDataCenterJs),
("color-scheme.js", colorSchemeJs),
("nav.js", navJs),
("expand-nav.js", expandNavJs),
("how-about.js", howAboutJs),
("search.html", searchHtml),
("search.js", searchJs),

View File

@ -150,6 +150,7 @@ are used in documentation generation, notably JS and CSS ones.
def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
def colorSchemeJs : String := include_str "../../static/color-scheme.js"
def navJs : String := include_str "../../static/nav.js"
def expandNavJs : String := include_str "../../static/expand-nav.js"
def howAboutJs : String := include_str "../../static/how-about.js"
def searchJs : String := include_str "../../static/search.js"
def instancesJs : String := include_str "../../static/instances.js"

View File

@ -33,6 +33,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
<script>{s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
[moduleConstant]
<script type="module" src={s!"{← getRoot}search.js"}></script>
<script type="module" src={s!"{← getRoot}expand-nav.js"}></script>
<script type="module" src={s!"{← getRoot}how-about.js"}></script>
<script type="module" src={s!"{← getRoot}instances.js"}></script>
<script type="module" src={s!"{← getRoot}importedBy.js"}></script>

View File

@ -95,6 +95,7 @@ def baseDirBlackList : HashSet String :=
"mathjax-config.js",
"navbar.html",
"nav.js",
"expand-nav.js",
"search.js",
"src",
"style.css"

View File

@ -72,6 +72,7 @@ library_facet docs (lib) : FilePath := do
basePath / "declaration-data.js",
basePath / "color-scheme.js",
basePath / "nav.js",
basePath / "expand-nav.js",
basePath / "how-about.js",
basePath / "search.js",
basePath / "mathjax-config.js",

17
static/expand-nav.js Normal file
View File

@ -0,0 +1,17 @@
document.querySelector('.navframe').addEventListener('load', function() {
// Get the current page URL without the suffix after #
var currentPageURL = window.location.href.split('#')[0];
// Get all detail elements
var as = document.querySelector('.navframe').contentWindow.document.body.querySelectorAll('a');
for (const a of as) {
if (a.href) {
var href = a.href.split('#')[0];
if (href === currentPageURL) {
a.style.fontStyle = 'italic';
var el = a.parentNode.closest('details');
while (el) {
el.open = true;
el = el.parentNode.closest('details');
}}}}
});