From 27a4eeedb907574a47e0e4a9dfdff67aacf514df Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 3 Mar 2026 23:09:20 +0000
Subject: [PATCH] fix: Article citation formatting (double period, spacing,
 number/pages)

Fix three sub-issues in Article citation rendering:
1. Double period after journal names ending in "." (e.g. "Lang..")
2. Missing space between journal name and volume number
3. Number running directly into "pp." with no separator

The fix conditionally appends "." after journal names, puts the number
in parentheses, and adds ", pp." before page ranges with a non-breaking
space. Applied to both HTML and TeX backends.

Fixes leanprover/verso#781

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .../VersoManual/Bibliography.lean             | 24 ++++++++++++++-----
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean
index 02876d10..5eb41f7b 100644
--- a/src/verso-manual/VersoManual/Bibliography.lean
+++ b/src/verso-manual/VersoManual/Bibliography.lean
@@ -184,7 +184,13 @@ def Citable.bibHtml [Monad m]
     return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". In " <em>{{← go p.booktitle}}"."</em>{{(← p.series.mapM go).map ({{" (" {{·}} ")" }}) |>.getD .empty}} }}
   | .article p =>
     let authors ← andList <$> p.authors.mapM go
-    return {{ {{authors}} " (" {{(← p.month.mapM go).map (· ++ {{" "}}) |>.getD .empty}}s!"{p.year}" "). " {{ link {{"“" {{← go p.title}} "”"}} }} ". " <em>{{← go p.journal}}"."</em> <strong>{{← go p.volume}}</strong>" "{{← go p.number}} {{p.pages.map (fun (x, y) => s!"pp. {x}–{y}") |>.getD .empty }}  "."}}
+    let journalDot := if (slugString p.journal).endsWith "." then "" else "."
+    let numberInl ← go p.number
+    let numberHtml : Html := if (slugString p.number).isEmpty then .empty
+                              else {{"(" {{numberInl}} ")"}}
+    let pagesHtml : Html := p.pages.map (fun (x, y) => {{", pp. " s!"{x}–{y}"}})
+                             |>.getD .empty
+    return {{ {{authors}} " (" {{(← p.month.mapM go).map (· ++ {{" "}}) |>.getD .empty}}s!"{p.year}" "). " {{ link {{"“" {{← go p.title}} "”"}} }} ". " <em>{{← go p.journal}}{{journalDot}}</em>" " <strong>{{← go p.volume}}</strong>{{numberHtml}}{{pagesHtml}}"."}}
   | .thesis p =>
     return {{ {{← go p.author}} s!", {p.year}. " <em>{{link (← go p.title)}}</em> ". " {{← go p.degree}} ", " {{← go p.university}} }}
   | .arXiv p =>
@@ -212,15 +218,21 @@ def Citable.bibTeX (go : Doc.Inline Genre.Manual → TeXT Manual (ReaderT Extens
      }
   | .article p =>
     let authors ← andListTeX <$> p.authors.mapM go
+    let journalDot := if (slugString p.journal).endsWith "." then "" else "."
+    let numberInl ← go p.number
+    let numberTeX : TeX := if (slugString p.number).isEmpty then .empty
+                            else \TeX{"(" \Lean{numberInl} ")"}
+    let pagesTeX : TeX := p.pages.map (fun (x, y) => \TeX{", pp.~" \Lean{toString x} "--" \Lean{toString y} })
+                           |>.getD .empty
     return \TeX{
        \Lean{authors}  " ("
        \Lean{ (← p.month.mapM go).map (fun x => \TeX{\Lean{x} " "}) |>.getD .empty  }
        \Lean{toString p.year} "). "
-       \Lean{ link \TeX{ "``" \Lean{← go p.title} "''" } } ". In "
-       \em{ \Lean{ ← go p.journal } "." }
-       \Lean{ ← go p.volume } " "
-       \Lean{ ← go p.number }
-       \Lean{ p.pages.map (fun (x, y) => \TeX{\Lean{toString x} "-" \Lean{toString y} }) |>.getD .empty }
+       \Lean{ link \TeX{ "``" \Lean{← go p.title} "''" } } ". "
+       \em{ \Lean{ ← go p.journal } \Lean{journalDot} }
+       "~" \textbf{ \Lean{ ← go p.volume } }
+       \Lean{numberTeX}
+       \Lean{pagesTeX}
        "."
      }
   | .thesis p =>