From eeffb498b829dcc68e6429e466acdcb99d893917 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Aug 2014 13:20:25 -0700
Subject: [PATCH] feat(frontends/lean/dependencies): send all missing files to
 standard error, closes #111

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/dependencies.cpp | 18 +++++++++---------
 src/frontends/lean/dependencies.h   |  2 +-
 src/shell/lean.cpp                  |  3 ++-
 3 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp
index 747eaa9642..944fb6ad43 100644
--- a/src/frontends/lean/dependencies.cpp
+++ b/src/frontends/lean/dependencies.cpp
@@ -12,18 +12,20 @@ Author: Leonardo de Moura
 #include "frontends/lean/scanner.h"
 
 namespace lean {
-void display_deps(environment const & env, std::ostream & out, char const * fname) {
+bool display_deps(environment const & env, std::ostream & out, std::ostream & err, char const * fname) {
     name import("import");
     name period(".");
     std::ifstream in(fname);
-    if (in.bad() || in.fail())
-        throw exception(sstream() << "failed to open file '" << fname << "'");
+    if (in.bad() || in.fail()) {
+        err << "failed to open file '" << fname << "'" << std::endl;
+        return false;
+    }
     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;
+    bool ok            = true;
     while (true) {
         scanner::token_kind t = scanner::token_kind::Identifier;
         try {
@@ -32,9 +34,7 @@ void display_deps(environment const & env, std::ostream & out, char const * fnam
             continue;
         }
         if (t == scanner::token_kind::Eof) {
-            if (ex)
-                ex->rethrow();
-            return;
+            return ok;
         } else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) {
             k = optional<unsigned>();
             import_prefix = true;
@@ -57,8 +57,8 @@ void display_deps(environment const & env, std::ostream & out, char const * fnam
                 import_prefix = true;
                 out << "\n";
             } catch (exception & new_ex) {
-                if (!ex)
-                    ex.reset(new_ex.clone());
+                err << "error: file '" << name_to_file(s.get_name_val()) << "' not found in the LEAN_PATH" << std::endl;
+                ok  = false;
             }
         } else {
             import_args   = false;
diff --git a/src/frontends/lean/dependencies.h b/src/frontends/lean/dependencies.h
index 9255cdeeaf..a96d8c481d 100644
--- a/src/frontends/lean/dependencies.h
+++ b/src/frontends/lean/dependencies.h
@@ -9,5 +9,5 @@ Author: Leonardo de Moura
 
 namespace lean {
 /** \brief Display in \c out all files the .lean file \c fname depends on */
-void display_deps(environment const & env, std::ostream & out, char const * fname);
+bool display_deps(environment const & env, std::ostream & out, std::ostream & err, char const * fname);
 }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 9d24f88561..2baa52cabe 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -266,7 +266,8 @@ int main(int argc, char ** argv) {
                 }
                 if (k == input_kind::Lean) {
                     if (only_deps) {
-                        display_deps(env, std::cout, argv[i]);
+                        if (!display_deps(env, std::cout, std::cerr, argv[i]))
+                            ok = false;
                     } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr, index_ptr)) {
                         ok = false;
                     }