# HG changeset patch
# User wenzelm
# Date 1390069485 -3600
# Node ID 04b443d54aee3643ccdbcb116a405966fccc4b6c
# Parent  8e82439758602bfcfab9624950005ea2e547c08d
tuned;

diff -r 8e8243975860 -r 04b443d54aee src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sat Jan 18 19:15:12 2014 +0100
+++ b/src/Pure/General/scan.scala	Sat Jan 18 19:24:45 2014 +0100
@@ -171,13 +171,10 @@
           var i = start
           var count = 0
           var finished = false
-          while (!finished) {
-            if (i < end && count < max_count) {
-              val n = matcher(i, end)
-              val sym = in.source.subSequence(i, i + n).toString
-              if (pred(sym)) { i += n; count += 1 }
-              else finished = true
-            }
+          while (!finished && i < end && count < max_count) {
+            val n = matcher(i, end)
+            val sym = in.source.subSequence(i, i + n).toString
+            if (pred(sym)) { i += n; count += 1 }
             else finished = true
           }
           if (count < min_count) Failure("bad input", in)
@@ -290,18 +287,11 @@
         var i = start
         var d = depth
         var finished = false
-        while (!finished) {
-          if (i < end) {
-            val n = matcher(i, end)
-            val sym = in.source.subSequence(i, i + n).toString
-
-            if (Symbol.is_open(sym)) { i += n; d += 1 }
-            else if (d > 0) {
-              i += n
-              if (Symbol.is_close(sym)) d -= 1
-            }
-            else finished = true
-          }
+        while (!finished && i < end) {
+          val n = matcher(i, end)
+          val sym = in.source.subSequence(i, i + n).toString
+          if (Symbol.is_open(sym)) { i += n; d += 1 }
+          else if (d > 0) { i += n; if (Symbol.is_close(sym)) d -= 1 }
           else finished = true
         }
         if (i == start) Failure("bad input", in)