feat: Add Book for bibliography

examples/textbook/DemoTextbook.lean

@@ -98,11 +98,12 @@ Cite works using {lean}`citet`, {lean}`citep`, or {lean}`citehere`.
 They take a name of a citable reference value as a parameter.
 References should be defined as values, typically in one module that is imported (similar to the role of a `.bib` file in LaTeX).
 
-Textual citations, as with {citet someThesis}[], look like this.
+Textual citations, as with {citet someBook}[], look like this.
 Parenthetical {citep someArXiv}[] looks like this.
 Use {lean}`citehere` to literally include the cite rather than making a margin note, e.g. {citehere somePaper}[].
 Literally-included cites are mostly useful when performing citation inside a margin note.
 
+
 # Section References
 %%%
 tag := "sec-ref"

examples/textbook/DemoTextbook/Papers.lean

@@ -8,21 +8,29 @@ open Verso.Genre.Manual
 
 -- Here, `inlines!` is a macro that parses a string constant into Verso inline elements
 
-def someThesis : Thesis where
+def someThesis : Bibliography.Thesis where
   title := inlines!"A Great Thesis"
   author := inlines!"A. Great Student"
   year := 2025
   university := inlines!"A University"
   degree := inlines!"Something"
 
-def somePaper : InProceedings where
+def somePaper : Bibliography.InProceedings where
   title := inlines!"Grommulation of Flying Lambdas"
   authors := #[inlines!"A. Great Student"]
   year := 2025
   booktitle := inlines!"Proceedings of the Best Conference Ever"
 
-def someArXiv : ArXiv where
+def someArXiv : Bibliography.ArXiv where
   title := inlines!"Grommulation of Flying Lambdas"
   authors := #[inlines!"A. Great Student"]
   year := 2025
   id := "...insert arXiv id here..."
+
+def someBook : Bibliography.Book where
+  title := inlines!"A Good Book"
+  authors := #[inlines!"A. Great Student"]
+  year := 2025
+  publisher := inlines!"Oxford University Press"
+  series := some (inlines!"Series Books", 42)
+  isbn := some "978-0-19-853779-3"

src/verso-manual/VersoManual/Bibliography.lean

@@ -53,6 +53,17 @@ structure Thesis where
   url : Option String := none
 deriving ToJson, FromJson, BEq, Hashable, Ord
 
+structure Book where
+  title : Doc.Inline Manual
+  authors : Array (Doc.Inline Manual)
+  year : Int
+  url : Option String := none
+  isbn : Option String := none -- TODO: make concrete type `ISBN10` or `ISBN13`
+  publisher : Doc.Inline Manual
+  edition : Option (Doc.Inline Manual) := none
+  series : Option ((Doc.Inline Manual) × Int) := none
+deriving ToJson, FromJson, BEq, Hashable, Ord
+
 structure ArXiv where
   title : Doc.Inline Manual
   authors : Array (Doc.Inline Manual)
@@ -77,6 +88,7 @@ inductive Citable where
   | thesis : Thesis → Citable
   | arXiv : ArXiv → Citable
   | article : Article → Citable
+  | book : Book → Citable
 deriving ToJson, FromJson, BEq, Hashable, Ord
 
 instance : Coe InProceedings Citable where
@@ -91,21 +103,25 @@ instance : Coe ArXiv Citable where
 instance : Coe Article Citable where
   coe := .article
 
+instance : Coe Book Citable where
+  coe := .book
+
 def Citable.authors : Citable → Array (Doc.Inline Manual)
-  | .inProceedings p | .arXiv p | .article p => p.authors
+  | .inProceedings p | .arXiv p | .article p | .book p => p.authors
   | .thesis p => #[p.author]
 
 def Citable.title : Citable → Doc.Inline Manual
-  | .inProceedings p | .arXiv p | .thesis p | .article p => p.title
+  | .inProceedings p | .arXiv p | .thesis p | .article p | .book p => p.title
 
 def Citable.year : Citable → Int
-  | .inProceedings p | .arXiv p | .thesis p | .article p => p.year
+  | .inProceedings p | .arXiv p | .thesis p | .article p | .book p => p.year
 
 def Citable.url : Citable → Option String
   | .inProceedings p => p.url
   | .thesis p => p.url
   | .arXiv p => some s!"https://arxiv.org/abs/{p.id}"
   | .article p => p.url
+  | .book p => p.url
 
 
 private def slugString : Doc.Inline Manual → String
@@ -158,7 +174,10 @@ def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT Exte
   match c with
   | .inProceedings p =>
     let authors ← andList <$> p.authors.mapM go
-    return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". In " <em>{{← go p.booktitle}}"."</em>{{(← p.series.mapM go).map ({{" (" {{·}} ")" }}) |>.getD .empty}} }}
+    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 }}  "."}}
@@ -167,6 +186,13 @@ def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT Exte
   | .arXiv p =>
     let authors ← andList <$> p.authors.mapM go
     return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". arXiv:" {{p.id}} }}
+  | .book p =>
+    let authors ← andList <$> p.authors.mapM go
+    return {{
+      {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". "
+      {{ p.series.map (λ (s, v) => {{ "Volume " <strong>s!"{v}"</strong> " of " /- TODO: insert series -/ ", "}}) |>.getD .empty }}
+      {{← go (p.publisher)}}". "
+    }}
 where
   wrap (content : Html) : Html := {{<span class="citation">{{content}}</span>}}
   link (title : Html) : Html :=