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,