src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Sun Nov 14 15:42:38 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Nov 14 17:46:41 2021 +0100
@@ -366,8 +366,13 @@
     val UNIMPORTANT = "unimportant"
   }
 
+
+  /* LaTeX */
+
   val Document_Latex = new Markup_Elem("document_latex")
 
+  val Latex_Output = new Markup_Elem("latex_output")
+
 
   /* Markdown document structure */