src/Pure/General/symbol.scala
changeset 73587 0af9e7e4476f
parent 73454 e53f4c5927a1
child 73602 ec52a1a6ed31
equal deleted inserted replaced
73586:ff7ce802be52 73587:0af9e7e4476f
   115     new Iterator[Symbol]
   115     new Iterator[Symbol]
   116     {
   116     {
   117       private val matcher = new Matcher(text)
   117       private val matcher = new Matcher(text)
   118       private var i = 0
   118       private var i = 0
   119       def hasNext: Boolean = i < text.length
   119       def hasNext: Boolean = i < text.length
   120       def next: Symbol =
   120       def next(): Symbol =
   121       {
   121       {
   122         val n = matcher(i, text.length)
   122         val n = matcher(i, text.length)
   123         val s =
   123         val s =
   124           if (n == 0) ""
   124           if (n == 0) ""
   125           else if (n == 1) {
   125           else if (n == 1) {