# HG changeset patch
# User wenzelm
# Date 1673614659 -3600
# Node ID c847442df7fe9a902480076e88ee945eff604ccb
# Parent  d756f4f78dc7c727fc19cd1ed948241b29143a9b
tuned;

diff -r d756f4f78dc7 -r c847442df7fe src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Fri Jan 13 13:10:44 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Fri Jan 13 13:57:39 2023 +0100
@@ -54,7 +54,7 @@
       tree match {
         case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
           val kind = Markup.Kind.unapply(props).getOrElse("cite")
-          val citations = Markup.Citations.unapply(props).getOrElse("")
+          val citations = Markup.Citations.get(props)
           Some(Value(kind, citations, body))
         case _ => None
       }