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 */