src/Pure/PIDE/markup.ML
changeset 74784 d2522bb4db1b
parent 74673 eae5fa0055bd
child 74786 543f932f64b8
--- a/src/Pure/PIDE/markup.ML	Sun Nov 14 15:42:38 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Nov 14 17:46:41 2021 +0100
@@ -149,6 +149,7 @@
   val document_markerN: string val document_marker: T
   val document_tagN: string val document_tag: string -> T
   val document_latexN: string val document_latex: T
+  val latex_outputN: string val latex_output: T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
   val markdown_bulletN: string val markdown_bullet: int -> T
@@ -569,8 +570,13 @@
 val (document_markerN, document_marker) = markup_elem "document_marker";
 val (document_tagN, document_tag) = markup_string "document_tag" nameN;
 
+
+(* LaTeX *)
+
 val (document_latexN, document_latex) = markup_elem "document_latex";
 
+val (latex_outputN, latex_output) = markup_elem "latex_output";
+
 
 (* Markdown document structure *)