diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 84eb05f..59ee753 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -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),
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 8fab52a..5c701ac 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -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"
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 192fb4b..979069c 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -33,6 +33,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
[moduleConstant]
+
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean
index ad8e570..5b8dbb1 100644
--- a/DocGen4/Process/Hierarchy.lean
+++ b/DocGen4/Process/Hierarchy.lean
@@ -95,6 +95,7 @@ def baseDirBlackList : HashSet String :=
"mathjax-config.js",
"navbar.html",
"nav.js",
+ "expand-nav.js",
"search.js",
"src",
"style.css"
diff --git a/lakefile.lean b/lakefile.lean
index eb0a39a..a609922 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -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",
diff --git a/static/expand-nav.js b/static/expand-nav.js
new file mode 100644
index 0000000..fd13ba6
--- /dev/null
+++ b/static/expand-nav.js
@@ -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');
+ }}}}
+});