@@ -127,12 +127,27 @@ def Citable.tag (c : Citable) : Slug :=
127127
128128def Citable.sortKey (c : Citable) := c.authors.map slugString |>.foldr (init := s! " { c.year} "", " ++ ·)
129129
130+ /--
131+ Returns a human-readable formatted list of authors in HTML, panics if the array is empty.
132+ -/
130133private def andList (xs : Array Html) : Html :=
131- if h : xs.size = 1 then xs[0 ]
134+ if h : xs.size = 0 then panic! "tried to construct empty list of authors"
135+ else if h : xs.size = 1 then xs[0 ]
132136 else if h : xs.size = 2 then xs[0 ] ++ " and " ++ xs[1 ]
133137 else
134138 open Html in
135- (xs.extract 0 (xs.size - 1 )).foldr (init := {{" and " {{xs.back!}} }}) (· ++ ", " ++ ·)
139+ (xs.extract 0 (xs.size - 1 )).foldr (init := {{" and " {{xs.back}} }}) (· ++ ", " ++ ·)
140+
141+ /--
142+ Returns a human-readable formatted list of authors in TeX, panics if the array is empty.
143+ -/
144+ private def andListTeX (xs : Array TeX) : TeX :=
145+ if h : xs.size = 0 then panic! "tried to construct empty list of authors"
146+ else if h : xs.size = 1 then xs[0 ]
147+ else if h : xs.size = 2 then xs[0 ] ++ " and " ++ xs[1 ]
148+ else
149+ open TeX in
150+ (xs.extract 0 (xs.size - 1 )).foldr (init := \TeX{" and " \Lean{xs.back} }) (· ++ ", " ++ ·)
136151
137152partial def Bibliography.lastName (inl : Doc.Inline Manual) : Doc.Inline Manual :=
138153 let ws := words inl
@@ -182,6 +197,55 @@ where
182197 | none => title
183198 | some u => {{<a href={{u}}>{{title}}</a>}}
184199
200+ open Verso.Doc.TeX in
201+ open Verso.Output.TeX in
202+ def Citable.bibTeX (go : Doc.Inline Genre.Manual → TeXT Manual (ReaderT ExtensionImpls IO) TeX) (c : Citable) : TeXT Manual (ReaderT ExtensionImpls IO) TeX := wrap <$> open TeX in do
203+ match c with
204+ | .inProceedings p =>
205+ let authors ← andListTeX <$> p.authors.mapM go
206+ return \TeX{
207+ \Lean{authors} ", "
208+ \Lean{toString p.year} ". "
209+ \Lean{ link \TeX{ "``" \Lean{← go p.title} "''" } } ". In "
210+ \em{ \Lean{ ← go p.booktitle } "." }
211+ \Lean{ (← p.series.mapM go).map (fun x => \TeX{" (" \Lean{x} ") " }) |>.getD .empty }
212+ }
213+ | .article p =>
214+ let authors ← andListTeX <$> p.authors.mapM go
215+ return \TeX{
216+ \Lean{authors} " ("
217+ \Lean{ (← p.month.mapM go).map (fun x => \TeX{\Lean{x} " " }) |>.getD .empty }
218+ \Lean{toString p.year} "). "
219+ \Lean{ link \TeX{ "``" \Lean{← go p.title} "''" } } ". In "
220+ \em{ \Lean{ ← go p.journal } "." }
221+ \Lean{ ← go p.volume } " "
222+ \Lean{ ← go p.number }
223+ \Lean{ p.pages.map (fun (x, y) => \TeX{\Lean{toString x} "-" \Lean{toString y} }) |>.getD .empty }
224+ "."
225+ }
226+ | .thesis p =>
227+ return \TeX{
228+ \Lean{← go p.author} ", "
229+ \Lean{toString p.year} ". "
230+ \em{ \Lean{ ← go p.title } } ". "
231+ \Lean{← go p.degree} ", "
232+ \Lean{← go p.university}
233+ }
234+ | .arXiv p =>
235+ let authors ← andListTeX <$> p.authors.mapM go
236+ return \TeX{
237+ \Lean{authors} ", "
238+ \Lean{toString p.year} ". "
239+ \Lean{ link \TeX{ "``" \Lean{← go p.title} "''" } } ". arXiv:"
240+ \Lean{p.id}
241+ }
242+ where
243+ wrap (content : TeX) : TeX := content
244+ link (title : TeX) : TeX :=
245+ match c.url with
246+ | none => title
247+ | some u => makeLink u title
248+
185249def Citable.inlineHtml [Monad m]
186250 (go : Doc.Inline Genre.Manual → HtmlT Manual m Html)
187251 (ps : List Citable)
@@ -210,6 +274,43 @@ where
210274 (· ++ {{<em>"et al" </em>}}) <$> go (Bibliography.lastName p.authors[0 ])
211275 else andList <$> p.authors.mapM (go ∘ Bibliography.lastName)
212276
277+ open Verso.Doc.TeX in
278+ def Citable.inlineTeX
279+ (go : Doc.Inline Genre.Manual → TeXT Manual (ReaderT ExtensionImpls IO) Output.TeX)
280+ (ps : List Citable)
281+ (fmt : Style) :
282+ TeXT Manual (ReaderT ExtensionImpls IO) TeX := open TeX in do
283+ match fmt with
284+ | .textual =>
285+ let out : Array TeX ← ps.toArray.mapM fun p => do
286+ let m ← p.bibTeX go
287+ pure <| \TeX{
288+ \Lean{ ← authorTeX p} " "
289+ \Lean{toString p.year}
290+ \Lean{Marginalia.TeX m}
291+ }
292+ pure <| andListTeX out
293+ | .parenthetical =>
294+ let out : Array TeX ← ps.toArray.mapM fun p => do
295+ let m ← p.bibTeX go
296+ pure <| \TeX{
297+ "(" \Lean{ ← authorTeX p} ", "
298+ \Lean{toString p.year} ") "
299+ \Lean{Marginalia.TeX m}
300+ }
301+ pure <| andListTeX out
302+ | .here => do
303+ pure <| andListTeX (← ps.toArray.mapM (·.bibTeX go))
304+ where
305+ authorTeX p := open TeX in do
306+ if p.authors.size = 0 then
307+ pure .empty
308+ else if h : p.authors.size = 1 then
309+ go <| Bibliography.lastName p.authors[0 ]
310+ else if h : p.authors.size > 3 then
311+ (· ++ \TeX{\em{"et al" } }) <$> go (Bibliography.lastName p.authors[0 ])
312+ else andListTeX <$> p.authors.mapM (go ∘ Bibliography.lastName)
313+
213314private def arrayOrd (ord : Ord α) : Ord (Array α) := inferInstance
214315
215316private partial def cmpCite : Json → Json → Ordering
@@ -254,7 +355,16 @@ inline_extension Inline.cite (citations : List Citable) (style : Style := .paren
254355 if citedSet.binSearchContains v.1 (cmpCite · · == .lt) then pure ()
255356 else modify (·.set `Manual.Bibliography <| citedSet.binInsert (cmpCite · · == .lt) v.1 )
256357 pure none -- TODO disambiguate years
257- toTeX := none
358+ toTeX :=
359+ open Verso.Output.TeX in
360+ some <| fun go _ data _content => do -- TODO repurpose "content" for e.g. "page 5"
361+ match FromJson.fromJson? data with
362+ | .error e => TeX.logError s! "Failed to deserialize citation/style: { e} "return .empty
363+ | .ok (v : Json × Style) =>
364+ match FromJson.fromJson? v.1 with
365+ | .error e => TeX.logError s! "Failed to deserialize citation: { e} "return .empty
366+ | .ok (v' : List Citable) =>
367+ Citable.inlineTeX go v' v.2
258368 extraCss := [Marginalia.css]
259369 toHtml :=
260370 open Verso.Output.Html in
0 commit comments