From a92401ae05054906bd21b070650dae7bfc1fa3f1 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Sat, 10 Feb 2024 20:16:20 +0100
Subject: [PATCH] fix: show summaries of posts at a reasonable length

---
 src/verso-blog/Verso/Genre/Blog/Basic.lean    | 42 ++++++++++++++++++-
 src/verso-blog/Verso/Genre/Blog/Generate.lean |  4 +-
 src/verso-blog/Verso/Genre/Blog/Theme.lean    |  1 +
 3 files changed, 42 insertions(+), 5 deletions(-)

diff --git a/src/verso-blog/Verso/Genre/Blog/Basic.lean b/src/verso-blog/Verso/Genre/Blog/Basic.lean
index bdf5360..21b62e2 100644
--- a/src/verso-blog/Verso/Genre/Blog/Basic.lean
+++ b/src/verso-blog/Verso/Genre/Blog/Basic.lean
@@ -215,8 +215,46 @@ 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
+private def sumArrayWith (f : α → Nat) (arr : Array α) : Nat := Id.run do
+  let mut sum := 0
+  for x in arr do
+    sum := sum + f x
+  sum
+
+/-- An approximate word count for summary length limits -/
+partial defmethod Inline.wordCount : Inline genre → Nat
+  | .code str
+  | .text str => str.split (Char.isWhitespace) |>.filter (!·.isEmpty) |>.length
+  | .emph content
+  | .link content ..
+  | .concat content
+  | .other _ content
+  | .footnote _ (content : Array (Inline genre))
+  | .bold content => sumArrayWith wordCount content
+  | .math .. => 1
+  | .linebreak .. => 0
+  | .image _ _ => 1
+
+partial defmethod Block.wordCount : Block genre → Nat
+    | .para contents => sumArrayWith (·.wordCount) contents
+    | .ul items
+    | .ol _ items => sumArrayWith (fun ⟨_, bs⟩ => sumArrayWith wordCount bs) items
+    | .dl items => sumArrayWith (fun ⟨is, bs⟩ => sumArrayWith (·.wordCount) is + sumArrayWith wordCount bs) items
+    | .blockquote items
+    | .concat items => sumArrayWith wordCount items
+    | .other _ content => sumArrayWith wordCount content
+    | .code _ _ _ str => str.split (Char.isWhitespace) |>.filter (!·.isEmpty) |>.length
+
+defmethod BlogPost.summary (post : BlogPost) : Array (Block Post) := Id.run do
+  let mut out := #[]
+  let mut words := 100
+  for b in post.contents.content do
+    let wc := b.wordCount
+    if out.isEmpty || wc < words then
+      out := out.push b
+      words := words - wc
+    else break
+  out
 
 partial def TraverseState.freshId (state : Blog.TraverseState) (path : List String) (hint : Lean.Name) : String := Id.run do
   let mut idStr := mangle (toString hint)
diff --git a/src/verso-blog/Verso/Genre/Blog/Generate.lean b/src/verso-blog/Verso/Genre/Blog/Generate.lean
index 7841627..2f49e50 100644
--- a/src/verso-blog/Verso/Genre/Blog/Generate.lean
+++ b/src/verso-blog/Verso/Genre/Blog/Generate.lean
@@ -186,9 +186,7 @@ def writeBlog (theme : Theme) (id : Lean.Name) (txt : Part Page) (posts : Array
   writePage theme pageParams
 where
   summarize (p : BlogPost) : GenerateM Html := do
-    let some block := p.summary
-      | return .empty
-    GenerateM.toHtml Post block
+    Html.seq <$> p.summary.mapM (GenerateM.toHtml Post)
 
 
 partial def Dir.generate (theme : Theme) (dir : Dir) : GenerateM Unit :=
diff --git a/src/verso-blog/Verso/Genre/Blog/Theme.lean b/src/verso-blog/Verso/Genre/Blog/Theme.lean
index acbb414..21c5100 100644
--- a/src/verso-blog/Verso/Genre/Blog/Theme.lean
+++ b/src/verso-blog/Verso/Genre/Blog/Theme.lean
@@ -168,6 +168,7 @@ def archiveEntry : Template := do
          }}
        }}
       {{summary}}
+      <a href={{target}} class="read-more">"Read more"</a>
     </li>
   }}]