feat: blog genre: show summaries of posts on archives pages

examples/website/DemoSite/Blog/Conditionals.lean

@@ -6,7 +6,7 @@ open DemoSite
 #doc (Post) "Conditional Expressions in Lean" =>
 
 %%%
-authors := ["Fictional Author"]
+authors := ["Fictional Author", "Another Fictional Author"]
 date := {year := 2024, month := 1, day := 15}
 categories := [examples, other]
 %%%

examples/website/static_files/style.css

@@ -89,6 +89,23 @@ div.metadata {
     margin-bottom: 1.5em;
 }
 
+.metadata .authors, .metadata .date {
+    display: inline-block;
+}
+
+.metadata .authors:has(+ .date)::after {
+    content: " | ";
+}
+
+
+.metadata .authors::before {
+    content: "By ";
+}
+
+.metadata .authors .author:has(+ .author)::after {
+    content: ", ";
+}
+
 h1, h2, h3, h4, h5, h6 {
     font-family: sans-serif;
 }

src/verso-blog/Verso/Genre/Blog/Basic.lean

@@ -215,6 +215,9 @@ defmethod BlogPost.postName [Monad m] [MonadConfig m] [MonadState TraverseState
 defmethod BlogPost.postName' [Monad m] [MonadConfig m] (post : BlogPost) : m String :=
   post.contents.postName'
 
+defmethod BlogPost.summary (post : BlogPost) : Option (Block Post) :=
+  post.contents.content.get? 0
+
 partial def TraverseState.freshId (state : Blog.TraverseState) (path : List String) (hint : Lean.Name) : String := Id.run do
   let mut idStr := mangle (toString hint)
   match state.usedIds.find? path with

src/verso-blog/Verso/Genre/Blog/Generate.lean

@@ -167,24 +167,28 @@ def writeBlog (theme : Theme) (id : Lean.Name) (txt : Part Page) (posts : Array
         pure <| some (addr, post)
       let postList := {{
         <ul class="post-list">
-          {{← catPosts.mapM fun (_addr, p) =>
-            theme.archiveEntryTemplate.render (.ofList [("path", ⟨.mk "..", #[]⟩), ("post", ⟨.mk p, #[]⟩)])}}
+          {{← catPosts.mapM fun (_addr, p) => do
+            theme.archiveEntryTemplate.render (.ofList [("path", ⟨.mk "..", #[]⟩), ("post", ⟨.mk p, #[]⟩), ("summary", ⟨.mk (← summarize p), #[]⟩)])}}
         </ul>
       }}
       let catParams := Template.Params.ofList [("title", cat.name), ("category", ⟨.mk cat, #[]⟩), ("posts", ⟨.mk postList, #[]⟩)]
       writePage theme catParams (template := theme.categoryTemplate)
 
   let postList := {{
     <ul class="post-list">
-      {{← posts.mapM fun p =>
-        theme.archiveEntryTemplate.render (.ofList [("post", ⟨.mk p, #[]⟩)])}}
+      {{← posts.mapM fun p => do
+        theme.archiveEntryTemplate.render (.ofList [("post", ⟨.mk p, #[]⟩), ("summary", ⟨.mk (← summarize p), #[]⟩)])}}
     </ul>
   }}
   let allCats : Post.Categories := .mk <| meta.categories.toArray.map fun (c, _) =>
     (c.slug, c)
   let pageParams : Template.Params := (← forPart txt).insert "posts" ⟨.mk postList, #[]⟩ |>.insert "categories" ⟨.mk allCats, #[]⟩
   writePage theme pageParams
-
+where
+  summarize (p : BlogPost) : GenerateM Html := do
+    let some block := p.summary
+      | return .empty
+    GenerateM.toHtml Post block
 
 
 partial def Dir.generate (theme : Theme) (dir : Dir) : GenerateM Unit :=

src/verso-blog/Verso/Genre/Blog/Theme.lean

@@ -133,21 +133,43 @@ def category : Template := do
 
 def archiveEntry : Template := do
   let post : BlogPost ← param "post"
+  let summary ← param "summary"
   let target ← if let some p := (← param? "path") then
       pure <| p ++ "/" ++ (← post.postName')
     else post.postName'
+  let catAddr ← do
+    if let some p := (← param? "path") then
+      pure <| fun slug => p ++ "/" ++ slug
+    else pure <| fun slug => slug
+
   return #[{{
-  <li>
-    <a href={{target}}>
-    {{
-    match post.contents.metadata.map (·.date) with
-    | some {year := y, month := m, day := d : Date} => {{<span class="date"> s!"{y}-{m}-{d}" </span> " — "}}
-    | none => Html.empty
-    }}
-    <span class="name">{{post.contents.titleString}}</span>
-    </a>
-  </li>
-}}]
+    <li>
+      <a href={{target}} class="title">
+        <span class="name">{{post.contents.titleString}}</span>
+      </a>
+      {{ match post.contents.metadata with
+         | none => Html.empty
+         | some md => {{
+          <div class="metadata">
+            <div class="authors">
+              {{(md : Post.PartMetadata).authors.map ({{<span class="author">{{Html.text true ·}}</span>}}) |>.toArray}}
+            </div>
+            <div class="date">
+              s!"{md.date.year}-{md.date.month}-{md.date.day}"
+            </div>
+            {{if md.categories.isEmpty then Html.empty
+              else {{
+                <ul class="categories">
+                  {{md.categories.toArray.map (fun cat => {{<li><a href=s!"{catAddr cat.slug}">{{cat.name}}</a></li>}})}}
+                </ul>
+              }}
+            }}
+          </div>
+         }}
+       }}
+      {{summary}}
+    </li>
+  }}]
 
 end Default