# HG changeset patch
# User wenzelm
# Date 1412190049 -7200
# Node ID d1fe47fe5401426659af4a76a6301a4f43c3d27d
# Parent  5f88c142676d3a7ab347008a97266e4be622a2a2
actually finish after closing, e.g. relevant for consecutive (**)(**);

diff -r 5f88c142676d -r d1fe47fe5401 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Tue Sep 30 22:43:20 2014 +0200
+++ b/src/Pure/General/scan.scala	Wed Oct 01 21:00:49 2014 +0200
@@ -185,7 +185,8 @@
           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 if (Symbol.is_close(sym) && d > 0) { i += n; d -= 1; if (d == 0) finished = true }
+          else if (d > 0) i += n
           else finished = true
         }
         if (i == start) Failure("bad input", in)
@@ -248,7 +249,7 @@
         var finished = false
         while (!finished) {
           if (try_parse("(*")) d += 1
-          else if (d > 0 && try_parse("*)")) d -= 1
+          else if (d > 0 && try_parse("*)")) { d -= 1; if (d == 0) finished = true }
           else if (d == 0 || !try_parse(comment_text)) finished = true
         }
         if (in.offset < rest.offset)