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