From dc6bd76b6059cc59b8f389b2ea08d4bbaeb5a3a2 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Mon, 17 Jul 2023 17:59:17 -0600
Subject: [PATCH] Revise pdf links to mirror directories.

---
 DocGen4/Output/Navbar.lean   | 7 ++++++-
 DocGen4/Process/NameExt.lean | 3 +--
 static/style.css             | 1 -
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 775524b..cc39fac 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -14,8 +14,13 @@ open Lean
 open scoped DocGen4.Jsx
 
 def moduleListFile (file : NameExt) : BaseHtmlM Html := do
+  let contents :=
+    if file.ext == .pdf then
+      <span>{s!"🗎 {file.getString!} (<a class=\"pdf\" href={← moduleNameExtToLink file}>pdf</a>)"}</span>
+    else
+      <a href={← moduleNameExtToLink file}>{file.getString!}</a>
   return <div class={if (← getCurrentName) == file.name then "nav_link visible" else "nav_link"}>
-    <a class={if file.ext == .pdf then "pdf" else ""} href={← moduleNameExtToLink file}>{file.getString!}</a>
+    {contents}
   </div>
 
 /--
diff --git a/DocGen4/Process/NameExt.lean b/DocGen4/Process/NameExt.lean
index 2966f40..d1be339 100644
--- a/DocGen4/Process/NameExt.lean
+++ b/DocGen4/Process/NameExt.lean
@@ -42,8 +42,7 @@ def cmp (n₁ n₂ : NameExt) : Ordering :=
   | ord => ord
 
 def getString! : NameExt → String
-  | ⟨str _ s, .html⟩ => s
-  | ⟨str _ s, .pdf⟩ => s ++ ".pdf"
+  | ⟨str _ s, _⟩ => s
   | _       => unreachable!
 
 end NameExt
diff --git a/static/style.css b/static/style.css
index ae00a45..f8b37b6 100644
--- a/static/style.css
+++ b/static/style.css
@@ -751,7 +751,6 @@ a:link, a:visited, a:active {
 
 a.pdf:link, a.pdf:visited, a.pdf:active {
     color:var(--link-pdf-color);
-    text-decoration: none
 }
 
 /** Show it on hover though. **/