From 93e83baa1bd9cdb30d3b9528a0b7b0da29f080fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 15 Sep 2014 10:09:42 -0700
Subject: [PATCH] fix(frontends/lean/parser): commit_upto invocation after
 'import'

---
 src/frontends/lean/parser.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 1120bc8cd..2211ec1a3 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -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();