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

feat(frontends/lean/dependencies): send all missing files to standard error, closes #111

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-29 13:20:25 -07:00
parent d7da307f85
commit eeffb498b8
3 changed files with 12 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/frontends/lean/dependencies.cpp
View file

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

2
src/frontends/lean/dependencies.h
View file

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

3
src/shell/lean.cpp
View file

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