# HG changeset patch
# User wenzelm
# Date 1673550548 -3600
# Node ID deb7dffb33406e6a3f0214a5d3ebac0634296186
# Parent  e47fb5cfef411f0b534d28c4cc57802f26108d1c
avoid confusion of markup element vs. property names;

diff -r e47fb5cfef41 -r deb7dffb3340 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jan 12 19:48:47 2023 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Jan 12 20:09:08 2023 +0100
@@ -155,7 +155,7 @@
   val latex_environmentN: string val latex_environment: string -> T
   val latex_headingN: string val latex_heading: string -> T
   val latex_bodyN: string val latex_body: string -> T
-  val latex_citeN: string val latex_cite: {kind: string, citation: string} -> T
+  val latex_citeN: string val latex_cite: {kind: string, citations: string} -> T
   val latex_index_itemN: string val latex_index_item: T
   val latex_index_entryN: string val latex_index_entry: string -> T
   val latex_delimN: string val latex_delim: string -> T
@@ -592,10 +592,10 @@
 val (latex_headingN, latex_heading) = markup_string "latex_heading" kindN;
 val (latex_bodyN, latex_body) = markup_string "latex_body" kindN;
 val (latex_citeN, _) = markup_elem "latex_cite";
-fun latex_cite {kind, citation} =
+fun latex_cite {kind, citations} =
   (latex_citeN,
     (if kind = "" then [] else [(kindN, kind)]) @
-    (if citation = "" then [] else [("citation", citation)]));
+    (if citations = "" then [] else [("citations", citations)]));
 val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item";
 val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN;
 val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN;
diff -r e47fb5cfef41 -r deb7dffb3340 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Jan 12 19:48:47 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Jan 12 20:09:08 2023 +0100
@@ -363,7 +363,7 @@
   val Latex_Tag = new Markup_String("latex_tag", NAME)
 
   val Latex_Cite = new Markup_Elem("latex_cite")
-  val Citation_ = new Properties.String("citation")
+  val Citations = new Properties.String("citations")
 
   val Latex_Index_Item = new Markup_Elem("latex_index_item")
   val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)
diff -r e47fb5cfef41 -r deb7dffb3340 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Jan 12 19:48:47 2023 +0100
+++ b/src/Pure/Thy/latex.ML	Thu Jan 12 20:09:08 2023 +0100
@@ -206,8 +206,8 @@
         if exists_string (fn c => c = ",") s
         then error ("Single citation expected, without commas" ^ Position.here pos)
         else ());
-    val citation = space_implode "," (map #1 citations);
-    val markup = Markup.latex_cite {kind = kind, citation = citation};
+    val citations' = space_implode "," (map #1 citations);
+    val markup = Markup.latex_cite {kind = kind, citations = citations'};
   in [XML.Elem (markup, location)] end;
 
 
diff -r e47fb5cfef41 -r deb7dffb3340 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Thu Jan 12 19:48:47 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Thu Jan 12 20:09:08 2023 +0100
@@ -54,8 +54,8 @@
       tree match {
         case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
           val kind = Markup.Kind.unapply(props).getOrElse("cite")
-          val citation = Markup.Citation_.unapply(props).getOrElse("")
-          Some(Value(kind, citation, body))
+          val citations = Markup.Citations.unapply(props).getOrElse("")
+          Some(Value(kind, citations, body))
         case _ => None
       }
   }