diff --git a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean index 0d29f06..c514317 100644 --- 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 index 1060751..3fd1e54 100644 --- 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 index cec8a18..7e82164 100644 --- 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 {{