proper treatment of XML.Wrapped_Elem, e.g. Markup.class_parameter;
--- a/src/Pure/Thy/presentation.scala Tue Jan 05 16:39:53 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Tue Jan 05 17:22:07 2021 +0100
@@ -98,6 +98,7 @@
def html_body(xml_body: XML.Body): XML.Body =
xml_body flatMap {
+ case XML.Wrapped_Elem(markup, _, body) => html_body(List(XML.Elem(markup, body)))
case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
val body1 = html_body(body)
if (elements.entity(kind)) {