From cac10aa7289fc91b3d306f47ed2b64693db7e523 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Dec 2015 19:59:11 -0500
Subject: [PATCH] fix(frontends/lean/parser): allow '...' token to be used in
 imports

Before this commit, we could not write

           import ...foo.b

We had to write

          import .. .foo.b

or

          import . ..foo.b
---
 src/frontends/lean/parser.cpp | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 4cda11adfb..3898ec49c0 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2165,12 +2165,22 @@ void parser::parse_imports() {
         next();
         while (true) {
             optional<unsigned> k;
-            while (curr_is_token(get_period_tk())) {
-                next();
-                if (!k)
-                    k = 0;
-                else
-                    k = *k + 1;
+            while (true) {
+                if (curr_is_token(get_period_tk())) {
+                    next();
+                    if (!k)
+                        k = 0;
+                    else
+                        k = *k + 1;
+                } else if (curr_is_token(get_ellipsis_tk())) {
+                    next();
+                    if (!k)
+                        k = 2;
+                    else
+                        k = *k + 3;
+                } else {
+                    break;
+                }
             }
             if (!curr_is_identifier())
                 break;