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)