diff -r f3a8476285c6 -r f231a7594e54 src/Pure/Thy/html.scala --- 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