src/Pure/PIDE/markup.scala
changeset 74786 543f932f64b8
parent 74784 d2522bb4db1b
child 74790 3ce6fb9db485
--- a/src/Pure/PIDE/markup.scala	Sun Nov 14 20:15:28 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Nov 14 20:40:41 2021 +0100
@@ -372,6 +372,8 @@
   val Document_Latex = new Markup_Elem("document_latex")
 
   val Latex_Output = new Markup_Elem("latex_output")
+  val Latex_Index_Item = new Markup_Elem("latex_index_item")
+  val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)
 
 
   /* Markdown document structure */