src/Pure/Thy/presentation.scala
changeset 73301 523806d71dea
parent 73299 45a34cc581b8
child 73364 c3589f2dff31
equal deleted inserted replaced
73300:32618ae1b65d 73301:523806d71dea
    96       else if (html_div(html)) List(HTML.div(c, html))
    96       else if (html_div(html)) List(HTML.div(c, html))
    97       else List(HTML.span(c, html))
    97       else List(HTML.span(c, html))
    98 
    98 
    99     def html_body(xml_body: XML.Body): XML.Body =
    99     def html_body(xml_body: XML.Body): XML.Body =
   100       xml_body flatMap {
   100       xml_body flatMap {
       
   101         case XML.Wrapped_Elem(markup, _, body) => html_body(List(XML.Elem(markup, body)))
   101         case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
   102         case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
   102           val body1 = html_body(body)
   103           val body1 = html_body(body)
   103           if (elements.entity(kind)) {
   104           if (elements.entity(kind)) {
   104             entity_link(props, body1) match {
   105             entity_link(props, body1) match {
   105               case Some(link) => List(link)
   106               case Some(link) => List(link)