author | wenzelm |
Fri, 13 Jan 2023 13:57:39 +0100 | |
changeset 76962 | c847442df7fe |
parent 76961 | d756f4f78dc7 |
child 76963 | a8566127d43b |
--- 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 }