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

feat(frontends/lean/dependencies): do not stop computing dependencies at error, compute as many as possible, and sign error in the end

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-29 12:34:37 -07:00
parent 3f50fd3ddd
commit bd3fb3489b
1 changed files with 18 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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