From bd3fb3489be1f1e6e7d9e79e7ef695da75ea13dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Aug 2014 12:34:37 -0700
Subject: [PATCH] feat(frontends/lean/dependencies): do not stop computing
 dependencies at error, compute as many as possible, and sign error in the end

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/dependencies.cpp | 28 ++++++++++++++++++----------
 1 file changed, 18 insertions(+), 10 deletions(-)

diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp
index 6fe1c931b..747eaa964 100644
--- a/src/frontends/lean/dependencies.cpp
+++ b/src/frontends/lean/dependencies.cpp
@@ -20,6 +20,7 @@ void display_deps(environment const & env, std::ostream & out, char const * fnam
         throw exception(sstream() << "failed to open file '" << fname << "'");
     scanner s(in, fname);
     optional<unsigned> k;
+    std::unique_ptr<exception> ex;
     std::string base = dirname(fname);
     bool import_prefix = false;
     bool import_args   = false;
@@ -31,6 +32,8 @@ void display_deps(environment const & env, std::ostream & out, char const * fnam
             continue;
         }
         if (t == scanner::token_kind::Eof) {
+            if (ex)
+                ex->rethrow();
             return;
         } else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) {
             k = optional<unsigned>();
@@ -42,16 +45,21 @@ void display_deps(environment const & env, std::ostream & out, char const * fnam
                 k = *k + 1;
         } else if ((import_prefix || import_args) && t == scanner::token_kind::Identifier) {
             import_args = true;
-            std::string m_name = find_file(base, k, name_to_file(s.get_name_val()), {".lean", ".olean", ".lua"});
-            int last_idx = m_name.find_last_of(".");
-            std::string rawname = m_name.substr(0, last_idx);
-            std::string ext = m_name.substr(last_idx);
-            if (ext == ".lean")
-                m_name = rawname + ".olean";
-            display_path(out, m_name);
-            k = optional<unsigned>();
-            import_prefix = true;
-            out << "\n";
+            try {
+                std::string m_name = find_file(base, k, name_to_file(s.get_name_val()), {".lean", ".olean", ".lua"});
+                int last_idx = m_name.find_last_of(".");
+                std::string rawname = m_name.substr(0, last_idx);
+                std::string ext = m_name.substr(last_idx);
+                if (ext == ".lean")
+                    m_name = rawname + ".olean";
+                display_path(out, m_name);
+                k = optional<unsigned>();
+                import_prefix = true;
+                out << "\n";
+            } catch (exception & new_ex) {
+                if (!ex)
+                    ex.reset(new_ex.clone());
+            }
         } else {
             import_args   = false;
             import_prefix = false;