max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/module_mgr): gracefully handle exceptions during dependency discovery

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-12 07:38:33 +01:00 • committed by Leonardo de Moura
parent df91ae3738
commit 130f80efff
1 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/module_mgr.cpp
View file

@ -404,12 +404,16 @@ module_mgr::get_snapshots_or_unchanged_module(module_id const &id, std::string c
}
std::vector<module_name> module_mgr::get_direct_imports(module_id const & id, std::string const & contents) {
scope_message_context scope("dependencies");
std::istringstream in(contents);
bool use_exceptions = true;
parser p(get_initial_env(), m_ios, nullptr, in, id, use_exceptions);
std::vector<std::pair<module_name, module_id>> deps;
return p.get_imports();
try {
scope_message_context scope("dependencies");
std::istringstream in(contents);
bool use_exceptions = true;
parser p(get_initial_env(), m_ios, nullptr, in, id, use_exceptions);
std::vector<std::pair<module_name, module_id>> deps;
return p.get_imports();
} catch (...) {
return {};
}
}
std::tuple<std::string, module_src, time_t> fs_module_vfs::load_module(module_id const & id, bool can_use_olean) {