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

fix(frontends/lean/parser): commit_upto invocation after 'import'

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-15 10:09:42 -07:00
parent feb4993f9c
commit 93e83baa1b
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1189,7 +1189,9 @@ void parser::parse_imports() {
buffer<module_name> olean_files;
buffer<name> lua_files;
std::string base = dirname(get_stream_name().c_str());
bool imported = false;
while (curr_is_token(g_import)) {
imported = true;
m_last_cmd_pos = pos();
next();
while (true) {
@ -1235,6 +1237,8 @@ void parser::parse_imports() {
s << f;
});
}
if (imported)
commit_info(1);
}
void parser::commit_info(unsigned line) {
@ -1260,7 +1264,6 @@ bool parser::parse_commands() {
display_warning_pos(pos());
regular_stream() << " imported file uses 'sorry'" << endl;
}
commit_info(1);
while (!done) {
protected_call([&]() {
check_interrupted();