diff -r ce9134bdc1d4 -r c03f381fd373 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu May 02 11:43:56 2019 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu May 02 14:05:59 2019 +0200
@@ -132,6 +132,7 @@
   val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
+  val document_markerN: string val document_marker: T
   val document_tagN: string val document_tag: string -> T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
@@ -521,6 +522,7 @@
 val (paragraphN, paragraph) = markup_elem "paragraph";
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
+val (document_markerN, document_marker) = markup_elem "document_marker";
 val (document_tagN, document_tag) = markup_string "document_tag" nameN;