src/Pure/Thy/html.scala
changeset 43489 132f99cc0a43
parent 43459 def9784a3316
child 43490 5e6f76cacb93
     1.1 --- a/src/Pure/Thy/html.scala	Tue Jun 21 12:53:55 2011 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Tue Jun 21 13:29:44 2011 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4              flush()
     1.5              ts += elem
     1.6            }
     1.7 -          val syms = Symbol.iterator(txt).map(_.toString)
     1.8 +          val syms = Symbol.iterator_string(txt)
     1.9            while (syms.hasNext) {
    1.10              val s1 = syms.next
    1.11              def s2() = if (syms.hasNext) syms.next else ""