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

feat(shell): use system_import for lua files provided in the command line (i.e., their code will be available for all threads)

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

7
src/shell/lean.cpp
View file

@ -184,15 +184,12 @@ int main(int argc, char ** argv) {
}
}
script_state S = lean::get_thread_script_state();
environment env = mode == lean_mode::Standard ? mk_environment(trust_lvl) : mk_hott_environment(trust_lvl);
io_state ios(lean::mk_simple_formatter());
if (quiet)
ios.set_option("verbose", false);
script_state S = lean::get_thread_script_state();
set_global_environment(S.get_state(), env);
set_global_io_state(S.get_state(), ios);
try {
bool ok = true;
for (int i = optind; i < argc; i++) {
@ -210,7 +207,7 @@ int main(int argc, char ** argv) {
ok = false;
} else if (k == input_kind::Lua) {
try {
S.dofile(argv[i]);
lean::system_import(argv[i]);
} catch (lean::exception & ex) {
::lean::display_error(regular(env, ios), nullptr, ex);
ok = false;

2
src/util/thread_script_state.cpp
View file

@ -40,7 +40,7 @@ void system_import(char const * fname) {
// Import file in all existing states
lock_guard<mutex> lk(g_state_mutex);
for (auto & s : g_states) {
s.import(fname);
s.import_explicit(fname);
}
}
{