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

feat(frontends/lean/parser): use system_import when processing Lean import command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-17 22:09:42 -07:00
parent b9a7cc41ef
commit 06002c5312
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/parser.cpp
View file

@ -989,11 +989,8 @@ void parser::parse_imports() {
} }
} }
m_env = import_modules(m_env, olean_files.size(), olean_files.data(), m_num_threads, true, m_ios); m_env = import_modules(m_env, olean_files.size(), olean_files.data(), m_num_threads, true, m_ios);
using_script([&](lua_State * L) { for (auto const & f : lua_files)
for (auto const & f : lua_files) { system_import(f.c_str());
to_script_state(L).import_explicit(f.c_str());
}
});
} }
bool parser::parse_commands() { bool parser::parse_commands() {