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

fix(library/module): bug in module import

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-23 16:23:47 -07:00
parent 879572ee7e
commit d30c600eb2
1 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/module.cpp
View file

@ -211,9 +211,11 @@ struct import_modules_fn {
r->m_module_idx = m_import_counter;
m_import_counter++;
std::swap(r->m_obj_code, code);
m_module_info.insert(mk_pair(mname, r));
for (auto i : imports) {
r->m_dependents.push_back(load_module_file(i));
auto d = load_module_file(i);
d->m_dependents.push_back(r);
}
if (imports.empty())
@ -344,7 +346,17 @@ struct import_modules_fn {
return env;
}
void store_direct_imports(unsigned num_modules, std::string const * modules) {
m_senv.update([&](environment const & env) -> environment {
module_ext ext = get_extension(env);
for (unsigned i = 0; i < num_modules; i++)
ext.m_direct_imports = list<std::string>(modules[i], ext.m_direct_imports);
return update(env, ext);
});
}
environment operator()(unsigned num_modules, std::string const * modules) {
store_direct_imports(num_modules, modules);
for (unsigned i = 0; i < num_modules; i++)
load_module_file(modules[i]);
process_asynch_tasks();