diff --git a/examples/textbook/DemoTextbook.lean b/examples/textbook/DemoTextbook.lean
index 8bd8b9ab..3464476b 100644
--- a/examples/textbook/DemoTextbook.lean
+++ b/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"
diff --git a/examples/textbook/DemoTextbook/Papers.lean b/examples/textbook/DemoTextbook/Papers.lean
index d5ce6179..d20e2924 100644
--- a/examples/textbook/DemoTextbook/Papers.lean
+++ b/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"
diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean
index ae61ce02..911e377e 100644
--- a/src/verso-manual/VersoManual/Bibliography.lean
+++ b/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 " {{← go p.booktitle}}"."{{(← p.series.mapM go).map ({{" (" {{·}} ")" }}) |>.getD .empty}} }}
+ return {{
+ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }}
+ ". In " {{← go p.booktitle}}"."{{(← 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}} "”"}} }} ". " {{← go p.journal}}"." {{← go p.volume}}" "{{← 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 " s!"{v}" " of " /- TODO: insert series -/ ", "}}) |>.getD .empty }}
+ {{← go (p.publisher)}}". "
+ }}
where
wrap (content : Html) : Html := {{{{content}}}}
link (title : Html) : Html :=