From b9a7cc41ef58b7b10f451c4cb98e417bfc809616 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Jun 2014 22:04:09 -0700
Subject: [PATCH] feat(shell): use system_import for lua files provided in the
 command line (i.e., their code will be available for all threads)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/shell/lean.cpp               | 7 ++-----
 src/util/thread_script_state.cpp | 2 +-
 2 files changed, 3 insertions(+), 6 deletions(-)

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<mutex> lk(g_state_mutex);
         for (auto & s : g_states) {
-            s.import(fname);
+            s.import_explicit(fname);
         }
     }
     {