src/Pure/PIDE/rendering.scala
changeset 74782 0a87ea7eb76f
parent 73359 d8a0e996614b
child 74887 56247fdb8bbb
--- a/src/Pure/PIDE/rendering.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -257,7 +257,7 @@
       Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE)
 
   val document_tag_elements =
-    Markup.Elements(Markup.Document_Tag.ELEMENT)
+    Markup.Elements(Markup.Document_Tag.name)
 
   val markdown_elements =
     Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,