actually finish after closing, e.g. relevant for consecutive (**)(**);
--- 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)