# HG changeset patch
# User wenzelm
# Date 1303394593 -7200
# Node ID 781c622af16a6b3355ff14878008659bc668d312
# Parent  5e7a7343ab11be6133ab803cee57ee0250edc2c6
more robust scanning of iterated comments, such as "(* (**) (**) *)";

diff -r 5e7a7343ab11 -r 781c622af16a src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Apr 21 12:56:27 2011 +0200
+++ b/src/Pure/General/scan.scala	Thu Apr 21 16:03:13 2011 +0200
@@ -220,16 +220,14 @@
     def comment: Parser[String] = new Parser[String]
     {
       val comment_text =
-        rep(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
-      val comment_open = "(*" ~ comment_text ^^^ ()
-      val comment_close = comment_text ~ "*)" ^^^ ()
+        rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
 
       def apply(in: Input) =
       {
         var rest = in
-        def try_parse(p: Parser[Unit]): Boolean =
+        def try_parse[A](p: Parser[A]): Boolean =
         {
-          parse(p, rest) match {
+          parse(p ^^^ (), rest) match {
             case Success(_, next) => { rest = next; true }
             case _ => false
           }
@@ -237,9 +235,9 @@
         var depth = 0
         var finished = false
         while (!finished) {
-          if (try_parse(comment_open)) depth += 1
-          else if (depth > 0 && try_parse(comment_close)) depth -= 1
-          else finished = true
+          if (try_parse("(*")) depth += 1
+          else if (depth > 0 && try_parse("*)")) depth -= 1
+          else if (depth == 0 || !try_parse(comment_text)) finished = true
         }
         if (in.offset < rest.offset && depth == 0)
           Success(in.source.subSequence(in.offset, rest.offset).toString, rest)