src/Pure/Thy/html.scala
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