src/Pure/Thy/html.scala
changeset 43548 f231a7594e54
parent 43511 d138e7482a1b
child 43661 39fdbd814c7f
     1.1 --- a/src/Pure/Thy/html.scala	Sat Jun 25 17:17:49 2011 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Sat Jun 25 18:15:36 2011 +0200
     1.3 @@ -60,10 +60,12 @@
     1.4    {
     1.5      def html_spans(tree: XML.Tree): XML.Body =
     1.6        tree match {
     1.7 -        case XML.Elem(Markup(name, _), ts) =>
     1.8 -          if (original_data)
     1.9 -            List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(html_spans)))))
    1.10 -          else List(span(name, ts.flatMap(html_spans)))
    1.11 +        case XML.Elem(m @ Markup(name, props), ts) =>
    1.12 +          val span_class =
    1.13 +            m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
    1.14 +          val html_span = span(span_class, ts.flatMap(html_spans))
    1.15 +          if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
    1.16 +          else List(html_span)
    1.17          case XML.Text(txt) =>
    1.18            val ts = new ListBuffer[XML.Tree]
    1.19            val t = new StringBuilder