From cbcaf5a48e49de45a75c1c9f8e916455c7dbde54 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 May 2015 22:10:15 -0700
Subject: [PATCH] fix(frontends/lean/scanner): block comments

fixes #600
---
 src/frontends/lean/scanner.cpp | 47 +++++++++++-----------------------
 src/frontends/lean/scanner.h   |  1 -
 tests/lean/run/600a.lean       |  3 +++
 tests/lean/run/600b.lean       |  3 +++
 tests/lean/run/600c.lean       | 12 +++++++++
 5 files changed, 33 insertions(+), 33 deletions(-)
 create mode 100644 tests/lean/run/600a.lean
 create mode 100644 tests/lean/run/600b.lean
 create mode 100644 tests/lean/run/600c.lean

diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 2d907e630..2647f9d34 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -216,42 +216,25 @@ void scanner::read_single_line_comment() {
     }
 }
 
-// Try to consume str, return true if success.
-// Throw a parser exception error_msg if end of file is found
-bool scanner::consume(char const * str, char const * error_msg) {
-    if (curr() == str[0]) {
-        next();
-        unsigned i = 1;
-        while (true) {
-            if (!str[i])
-                return true;
-            check_not_eof(error_msg);
-            if (curr_next() != str[i])
-                return false;
-            i++;
-        }
-    } else {
-        return false;
-    }
-}
-
-static char const * g_begin_comment_block = "/-";
-static char const * g_end_comment_block = "-/";
-static char const * g_end_error_block_msg = "unexpected end of comment block";
-
 void scanner::read_comment_block() {
     unsigned nesting = 1;
     while (true) {
-        if (consume(g_begin_comment_block, g_end_error_block_msg)) {
-            nesting++;
-        }
-        if (consume(g_end_comment_block, g_end_error_block_msg)) {
-            nesting--;
-            if (nesting == 0)
-                return;
-        }
-        check_not_eof(g_end_error_block_msg);
+        char c = curr();
+        check_not_eof("unexpected end of comment block");
         next();
+        if (c == '/') {
+            if (curr() == '-') {
+                next();
+                nesting++;
+            }
+        } else if (c == '-') {
+            if (curr() == '/') {
+                next();
+                nesting--;
+                if (nesting == 0)
+                    return;
+            }
+        }
     }
 }
 
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 07366f8ef..367f43abb 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -53,7 +53,6 @@ protected:
     bool is_next_digit();
     bool is_next_id_rest();
     void move_back(unsigned offset, unsigned u_offset);
-    bool consume(char const * str, char const * error_msg);
     void read_single_line_comment();
     void read_comment_block();
     void read_until(char const * end_str, char const * error_msg);
diff --git a/tests/lean/run/600a.lean b/tests/lean/run/600a.lean
new file mode 100644
index 000000000..b01a92136
--- /dev/null
+++ b/tests/lean/run/600a.lean
@@ -0,0 +1,3 @@
+/- - -/
+
+print "ok"
diff --git a/tests/lean/run/600b.lean b/tests/lean/run/600b.lean
new file mode 100644
index 000000000..5434688c2
--- /dev/null
+++ b/tests/lean/run/600b.lean
@@ -0,0 +1,3 @@
+/- --/
+
+print "ok"
diff --git a/tests/lean/run/600c.lean b/tests/lean/run/600c.lean
new file mode 100644
index 000000000..fc503a7ed
--- /dev/null
+++ b/tests/lean/run/600c.lean
@@ -0,0 +1,12 @@
+/- /- -/ -/
+/- - /--/-/
+/-/-/--/-/-/
+/--/
+/------------/
+/---/
+/- ---/
+/-
+-/
+
+----/
+print "ok"