# HG changeset patch
# User wenzelm
# Date 1609863727 -3600
# Node ID 523806d71deae5e09b826de426bde722f51fbf03
# Parent  32618ae1b65d18d301f75187f0cff0b2511976fb
proper treatment of XML.Wrapped_Elem, e.g. Markup.class_parameter;

diff -r 32618ae1b65d -r 523806d71dea src/Pure/Thy/presentation.scala
--- 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)) {