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