diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 3e146f88f..6ce97cdf5 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -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; diff --git a/src/util/thread_script_state.cpp b/src/util/thread_script_state.cpp index b720a1f4b..73923ef1e 100644 --- a/src/util/thread_script_state.cpp +++ b/src/util/thread_script_state.cpp @@ -40,7 +40,7 @@ void system_import(char const * fname) { // Import file in all existing states lock_guard lk(g_state_mutex); for (auto & s : g_states) { - s.import(fname); + s.import_explicit(fname); } } {