From 327fdf0ddd11384ace8fde97d6266c4429bc1cfa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 13 Dec 2022 18:58:02 +0100
Subject: [PATCH] feat: short names in side bar

---
 DocGen4/Output/Base.lean   | 2 +-
 DocGen4/Output/Navbar.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 75966d0..b7d7d5f 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -108,7 +108,7 @@ def moduleNameToLink (n : Name) : BaseHtmlM String := do
 Returns the HTML doc-gen4 link to a module name.
 -/
 def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
-  pure <a href={←moduleNameToLink module}>{module.toString}</a>
+  pure <a href={←moduleNameToLink module}>{module.getString!}</a>
 
 /--
 Returns the LeanInk link to a module name.
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index f5d2612..fb5fbe3 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -33,7 +33,7 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
     if h.isFile then
       <summary>{←moduleToHtmlLink h.getName}</summary>
     else
-      <summary>{h.getName.toString}</summary>
+      <summary>{h.getName.getString!}</summary>
 
   pure
     <details class="nav_sect" "data-path"={moduleLink} [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>