src/Pure/PIDE/markup.scala
changeset 76956 e47fb5cfef41
parent 76955 3f25c28c4257
child 76957 deb7dffb3340
--- a/src/Pure/PIDE/markup.scala	Thu Jan 12 16:01:49 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Jan 12 19:48:47 2023 +0100
@@ -363,7 +363,7 @@
   val Latex_Tag = new Markup_String("latex_tag", NAME)
 
   val Latex_Cite = new Markup_Elem("latex_cite")
-  val Cite_Location = new Properties.String("cite_location")
+  val Citation_ = new Properties.String("citation")
 
   val Latex_Index_Item = new Markup_Elem("latex_index_item")
   val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)