| changeset 38231 | 968844caaff9 |
| parent 38230 | ed147003de4b |
| child 38444 | 796904799f4d |
--- a/src/Pure/Thy/html.scala Sat Aug 07 22:09:52 2010 +0200 +++ b/src/Pure/Thy/html.scala Sat Aug 07 22:43:57 2010 +0200 @@ -53,7 +53,7 @@ def spans(tree: XML.Tree): List[XML.Tree] = tree match { case XML.Elem(Markup(name, _), ts) => - List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans))))) + List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(spans))))) case XML.Text(txt) => val ts = new ListBuffer[XML.Tree] val t = new StringBuilder