avoid confusion of markup element vs. property names;
--- 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;
--- 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)
--- 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;
--- 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
}
}