michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/parser): allow '...' token to be used in imports

Browse source 
Before this commit, we could not write

           import ...foo.b

We had to write

          import .. .foo.b

or

          import . ..foo.b
This commit is contained in:
Leonardo de Moura 2015-12-26 19:59:11 -05:00
parent 2a5a904416
commit cac10aa728
1 changed files with 16 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/frontends/lean/parser.cpp
View file

@ -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;