From 924be4c7d87cb442a429390bca422002c4ede0d4 Mon Sep 17 00:00:00 2001
From: "Alex J. Best" <alex.j.best@gmail.com>
Date: Mon, 18 Sep 2023 22:03:40 +0100
Subject: [PATCH] feat: expand the current file in the navbar

---
 DocGen4/Output.lean            |  1 +
 DocGen4/Output/Base.lean       |  1 +
 DocGen4/Output/Template.lean   |  1 +
 DocGen4/Process/Hierarchy.lean |  1 +
 lakefile.lean                  |  1 +
 static/expand-nav.js           | 17 +++++++++++++++++
 6 files changed, 22 insertions(+)
 create mode 100644 static/expand-nav.js

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
         <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>
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');
+                }}}}
+});