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 :=