feat: customizable nav bar

The nav bar can now get an optional "home" link, and pages can be hidden
leanprover · Jan 5, 2024 · fbf9662 · fbf9662
1 parent a283d41
commit fbf9662
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 4 deletions.
diff --git a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean
@@ -85,9 +85,12 @@ structure TraverseState where
   stylesheets : Lean.HashSet String := {}
   errors : Lean.HashSet String := {}
 
+structure Page.Meta where
+  /-- Whether to hide this page/part from navigation entries -/
+  showInNav : Bool := true
 
 def Page : Genre where
-  PartMetadata := Empty
+  PartMetadata := Page.Meta
   Block := Blog.BlockExt
   Inline := Blog.InlineExt
   TraverseContext := Blog.TraverseContext

diff --git a/src/leanblog/LeanDoc/Genre/Blog/Template.lean b/src/leanblog/LeanDoc/Genre/Blog/Template.lean
@@ -127,7 +127,7 @@ def blogGenreHtml (g : Genre) [MonadConfig (HtmlT g IO)] [MonadPath (HtmlT g IO)
   block := eq1 ▸ blockHtml g
   inline := eq2 ▸ inlineHtml g eq3
 
-instance : GenreHtml Page IO := blogGenreHtml Page rfl rfl rfl (fun _ m => nomatch m)
+instance : GenreHtml Page IO := blogGenreHtml Page rfl rfl rfl fun go _metadata part => go part
 instance : GenreHtml Post IO := blogGenreHtml Post rfl rfl rfl fun go _metadata part => go part
 
 namespace LeanDoc.Genre.Blog.Template

diff --git a/src/leanblog/LeanDoc/Genre/Blog/Theme.lean b/src/leanblog/LeanDoc/Genre/Blog/Theme.lean
@@ -31,7 +31,10 @@ def dirLinks : Site → TemplateM (Array Html)
   | .page _ _ subs =>
     subs.filterMapM fun
       | .page name _id txt .. | .blog name _id txt .. =>
-        pure <| some {{<li><a href={{"/" ++ name}}>{{txt.titleString}}</a></li>}}
+        if txt.metadata.map (·.showInNav) |>.getD true then
+          pure <| some {{<li><a href={{"/" ++ name}}>{{txt.titleString}}</a></li>}}
+        else
+          pure none
       | .static .. => pure none
   | .blog _ _ subs =>
     subs.mapM fun s => do
@@ -43,10 +46,11 @@ where
     let dest' ← relative dest
     return String.join (dest'.map (· ++ "/"))
 
-def topNav : Template := do
+def topNav (homeLink : Option String := none) : Template := do
     pure {{
       <nav class="top" role="navigation">
         <ol>
+          {{homeLink.map ({{<li class="home"><a href="/">s!"{·}"</a></li>}}) |>.getD .empty}}
           {{ ← dirLinks (← read).site }}
         </ol>
       </nav>