tuned signature;
authorwenzelm
Fri, 20 Jan 2023 13:31:58 +0100
changeset 77024 6e90e84f7e7c
parent 77023 474a07221c27
child 77025 34219d664854
tuned signature;
src/Pure/Thy/bibtex.scala
src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Jan 20 13:11:58 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Jan 20 13:31:58 2023 +0100
@@ -745,10 +745,10 @@
         case _ => None
       }
 
-    sealed case class Inner(kind: String, citation: String, location: XML.Body, pos: Position.T) {
+    sealed case class Inner(kind: String, citations: String, location: XML.Body, pos: Position.T) {
       def nocite: Inner = copy(kind = NOCITE, location = Nil)
 
-      override def toString: String = citation
+      override def toString: String = citations
     }
 
     sealed case class Outer(kind: String, body: String, start: Isar_Token.Pos) {
--- a/src/Pure/Thy/latex.scala	Fri Jan 20 13:11:58 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Fri Jan 20 13:31:58 2023 +0100
@@ -225,7 +225,7 @@
         latex_macro0(inner.kind) :::
         (if (inner.location.isEmpty) Nil
          else XML.string("[") ::: inner.location ::: XML.string("]")) :::
-        XML.string("{" + inner.citation + "}")
+        XML.string("{" + inner.citations + "}")
 
       if (inner.pos.isEmpty) body
       else List(XML.Elem(Markup.Latex_Output(inner.pos), body))