src/Pure/Thy/html.scala
changeset 36011 3ff725ac13a4
parent 34137 6cc9a0cbaf55
child 36012 0614676f14d4
     1.1 --- a/src/Pure/Thy/html.scala	Mon Mar 29 01:07:01 2010 -0700
     1.2 +++ b/src/Pure/Thy/html.scala	Mon Mar 29 22:43:56 2010 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4            flush()
     1.5            ts + elem
     1.6          }
     1.7 -        val syms = Symbol.elements(txt).map(_.toString)
     1.8 +        val syms = Symbol.iterator(txt).map(_.toString)
     1.9          while (syms.hasNext) {
    1.10            val s1 = syms.next
    1.11            def s2() = if (syms.hasNext) syms.next else ""