actually finish after closing, e.g. relevant for consecutive (**)(**);
authorwenzelm
Wed, 01 Oct 2014 21:00:49 +0200
changeset 58505 d1fe47fe5401
parent 58504 5f88c142676d
child 58506 11c652544108
child 58523 937c479e62fe
actually finish after closing, e.g. relevant for consecutive (**)(**);
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)