From c7338a8eaba6d788a6a64d1375a90b5820bd3239 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Jan 2014 14:37:28 -0800
Subject: [PATCH] chore(frontends/lean/scanner): remove dead code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/scanner.cpp | 28 ----------------------------
 src/frontends/lean/scanner.h   |  1 -
 2 files changed, 29 deletions(-)

diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index adf2ac41f..d7424d59c 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -138,34 +138,6 @@ bool scanner::check_next_is_digit() {
     return r;
 }
 
-void scanner::read_comment() {
-    int nest = 1;
-    while (true) {
-        if (curr() == '*') {
-            next();
-            if (curr() == ')') {
-                next();
-                nest--;
-                if (nest == 0)
-                    return;
-            }
-        } else if (curr() == '(') {
-            next();
-            if (curr() == '*') {
-                next();
-                nest++;
-            }
-        } else if (curr() == '\n') {
-            new_line();
-            next();
-        } else if (curr() == EOF) {
-            throw_exception("unexpected end of comment");
-        } else {
-            next();
-        }
-    }
-}
-
 void scanner::read_single_line_comment() {
     while (true) {
         if (curr() == '\n') {
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 3d3e784d7..9b6216d78 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -46,7 +46,6 @@ protected:
     void  next();
     bool  check_next(char c);
     bool  check_next_is_digit();
-    void  read_comment();
     void  read_single_line_comment();
     name  mk_name(name const & curr, std::string const & buf, bool only_digits);
     token read_a_symbol();