--- a/src/Pure/PIDE/markup.scala Sat Nov 20 19:39:22 2021 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Nov 20 20:42:41 2021 +0100
@@ -377,6 +377,9 @@
val Latex_Environment = new Markup_String("latex_environment", NAME)
val Latex_Heading = new Markup_String("latex_heading", KIND)
val Latex_Body = new Markup_String("latex_body", KIND)
+ val Latex_Delim = new Markup_String("latex_delim", NAME)
+ val Latex_Tag = new Markup_String("latex_tag", NAME)
+
val Latex_Index_Item = new Markup_Elem("latex_index_item")
val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)