diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 8463823ccb..da1fdcbcd9 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp
-  notation.cpp frontend_elaborator.cpp)
+  notation.cpp frontend_elaborator.cpp register_module.cpp)
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 385d247ff7..141c71087a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -19,8 +19,10 @@ Author: Leonardo de Moura
 #include "util/scoped_map.h"
 #include "util/exception.h"
 #include "util/sstream.h"
-#include "util/sexpr/option_declarations.h"
+#include "util/script_state.h"
+#include "util/script_exception.h"
 #include "util/interrupt.h"
+#include "util/sexpr/option_declarations.h"
 #include "kernel/normalizer.h"
 #include "kernel/type_checker.h"
 #include "kernel/free_vars.h"
@@ -31,7 +33,7 @@ Author: Leonardo de Moura
 #include "library/arith/arith.h"
 #include "library/io_state.h"
 #include "library/placeholder.h"
-#include "library/script_evaluator.h"
+#include "library/kernel_bindings.h"
 #include "library/elaborator/elaborator_exception.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/frontend_elaborator.h"
@@ -131,7 +133,7 @@ class parser::imp {
     pos_info            m_last_cmd_pos;
     pos_info            m_last_script_pos;
 
-    script_evaluator *  m_script_evaluator;
+    script_state *      m_script_state;
 
     bool                m_verbose;
     bool                m_show_errors;
@@ -1404,7 +1406,7 @@ class parser::imp {
         try {
             if (m_verbose)
                 regular(m_frontend) << "Importing file '" << fname << "'" << endl;
-            parser import_parser(m_frontend, in, m_script_evaluator, true /* use exceptions */, false /* not interactive */);
+            parser import_parser(m_frontend, in, m_script_state, true /* use exceptions */, false /* not interactive */);
             import_parser();
         } catch (interrupted &) {
             throw;
@@ -1591,21 +1593,25 @@ class parser::imp {
 
     void parse_script() {
         m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos());
-        if (!m_script_evaluator)
+        if (!m_script_state)
             throw exception("failed to execute Lua script, parser does not have a Lua interpreter");
         std::string script_code = m_scanner.get_str_val();
         next();
-        m_script_evaluator->dostring(script_code.c_str(), m_frontend.get_environment(), m_frontend.get_state());
+        m_script_state->apply([&](lua_State * L) {
+                set_io_state    set1(L, m_frontend.get_state());
+                set_environment set2(L, m_frontend.get_environment());
+                dostring(L, script_code.c_str());
+            });
     }
 
 public:
-    imp(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive):
+    imp(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive):
         m_frontend(fe),
         m_scanner(in),
         m_elaborator(fe),
         m_use_exceptions(use_exceptions),
         m_interactive(interactive) {
-        m_script_evaluator = S;
+        m_script_state = S;
         updt_options();
         m_found_errors = false;
         m_num_local_decls = 0;
@@ -1689,7 +1695,7 @@ public:
     }
 };
 
-parser::parser(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
+parser::parser(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
     parser::imp::show_prompt(interactive, fe);
     m_ptr.reset(new imp(fe, in, S, use_exceptions, interactive));
 }
@@ -1705,7 +1711,7 @@ expr parser::parse_expr() {
     return m_ptr->parse_expr_main();
 }
 
-shell::shell(frontend & fe, script_evaluator * S):m_frontend(fe), m_script_evaluator(S) {
+shell::shell(frontend & fe, script_state * S):m_frontend(fe), m_script_state(S) {
 }
 
 shell::~shell() {
@@ -1721,34 +1727,34 @@ bool shell::operator()() {
         add_history(input);
         std::istringstream strm(input);
         {
-            parser p(m_frontend, strm, m_script_evaluator, false, false);
+            parser p(m_frontend, strm, m_script_state, false, false);
             if (!p())
                 errors = true;
         }
         free(input);
     }
 #else
-    parser p(m_frontend, std::cin, m_script_evaluator, false, true);
+    parser p(m_frontend, std::cin, m_script_state, false, true);
     return p();
 #endif
 }
 
-bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
+bool parse_commands(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
     return parser(fe, in, S, use_exceptions, interactive)();
 }
 
-bool parse_commands(environment const & env, io_state & st, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
+bool parse_commands(environment const & env, io_state & st, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
     frontend f(env, st);
     bool r = parse_commands(f, in, S, use_exceptions, interactive);
     st = f.get_state();
     return r;
 }
 
-expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions) {
+expr parse_expr(frontend & fe, std::istream & in, script_state * S, bool use_exceptions) {
     return parser(fe, in, S, use_exceptions).parse_expr();
 }
 
-expr parse_expr(environment const & env, io_state & st, std::istream & in, script_evaluator * S, bool use_exceptions) {
+expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S, bool use_exceptions) {
     frontend f(env, st);
     expr r = parse_expr(f, in, S, use_exceptions);
     st = f.get_state();
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 7435c2e2d6..fd7b7ea184 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 
 namespace lean {
-class script_evaluator;
+class script_state;
 class frontend;
 class io_state;
 class environment;
@@ -17,7 +17,7 @@ class parser {
     class imp;
     std::unique_ptr<imp> m_ptr;
 public:
-    parser(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions = true, bool interactive = false);
+    parser(frontend & fe, std::istream & in, script_state * S, bool use_exceptions = true, bool interactive = false);
     ~parser();
 
     /** \brief Parse a sequence of commands */
@@ -29,17 +29,17 @@ public:
 
 /** \brief Implements the Read Eval Print loop */
 class shell {
-    frontend &                m_frontend;
-    script_evaluator *        m_script_evaluator;
+    frontend &            m_frontend;
+    script_state *        m_script_state;
 public:
-    shell(frontend & fe, script_evaluator * S);
+    shell(frontend & fe, script_state * S);
     ~shell();
 
     bool operator()();
 };
 
-bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
-bool parse_commands(environment const & env, io_state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
-expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
-expr parse_expr(environment const & env, io_state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
+bool parse_commands(frontend & fe, std::istream & in, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false);
+bool parse_commands(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false);
+expr parse_expr(frontend & fe, std::istream & in, script_state * S = nullptr, bool use_exceptions = true);
+expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true);
 }
diff --git a/src/frontends/lua/frontend_lean.cpp b/src/frontends/lean/register_module.cpp
similarity index 88%
rename from src/frontends/lua/frontend_lean.cpp
rename to src/frontends/lean/register_module.cpp
index 270d4239ec..71e81ecf2b 100644
--- a/src/frontends/lua/frontend_lean.cpp
+++ b/src/frontends/lean/register_module.cpp
@@ -6,18 +6,19 @@ Author: Leonardo de Moura
 */
 #include <sstream>
 #include "util/lua.h"
+#include "util/script_state.h"
 #include "util/sexpr/options.h"
 #include "library/io_state.h"
 #include "library/kernel_bindings.h"
 #include "frontends/lean/parser.h"
-#include "frontends/lua/leanlua_state.h"
+#include "frontends/lean/frontend.h"
 
 namespace lean {
 /** \see parse_lean_expr */
 static int parse_lean_expr_core(lua_State * L, ro_environment const & env, io_state & st) {
     char const * src = luaL_checkstring(L, 1);
     std::istringstream in(src);
-    leanlua_state S   = to_leanlua_state(L);
+    script_state S   = to_script_state(L);
     push_expr(L, parse_expr(env, st, in, &S));
     return 1;
 }
@@ -73,7 +74,7 @@ static int parse_lean_expr(lua_State * L) {
 static void parse_lean_cmds_core(lua_State * L, rw_environment & env, io_state & st) {
     char const * src = luaL_checkstring(L, 1);
     std::istringstream in(src);
-    leanlua_state S   = to_leanlua_state(L);
+    script_state S   = to_script_state(L);
     parse_commands(env, st, in, &S);
 }
 
@@ -117,8 +118,18 @@ static int parse_lean_cmds(lua_State * L) {
     }
 }
 
+static int mk_environment(lua_State * L) {
+    frontend f;
+    return push_environment(L, f.get_environment());
+}
+
 void open_frontend_lean(lua_State * L) {
-    SET_GLOBAL_FUN(parse_lean_expr,   "parse_lean");
-    SET_GLOBAL_FUN(parse_lean_cmds,   "parse_lean_cmds");
+    SET_GLOBAL_FUN(mk_environment,  "environment");
+    SET_GLOBAL_FUN(parse_lean_expr, "parse_lean");
+    SET_GLOBAL_FUN(parse_lean_cmds, "parse_lean_cmds");
+}
+
+void register_frontend_lean_module() {
+    script_state::register_module(open_frontend_lean);
 }
 }
diff --git a/src/frontends/lua/frontend_lean.h b/src/frontends/lean/register_module.h
similarity index 87%
rename from src/frontends/lua/frontend_lean.h
rename to src/frontends/lean/register_module.h
index d456ed43e4..be5436e1f9 100644
--- a/src/frontends/lua/frontend_lean.h
+++ b/src/frontends/lean/register_module.h
@@ -8,4 +8,5 @@ Author: Leonardo de Moura
 #include <lua.hpp>
 namespace lean {
 void open_frontend_lean(lua_State * L);
+void register_frontend_lean_module();
 }
diff --git a/src/frontends/lua/CMakeLists.txt b/src/frontends/lua/CMakeLists.txt
index d718e57f6c..c4dde5af29 100644
--- a/src/frontends/lua/CMakeLists.txt
+++ b/src/frontends/lua/CMakeLists.txt
@@ -1,3 +1,3 @@
-add_library(leanlua leanlua_state.cpp frontend_lean.cpp)
+add_library(leanlua register_modules.cpp)
 
 target_link_libraries(leanlua ${LEAN_LIBS})
diff --git a/src/frontends/lua/lean.lua b/src/frontends/lua/lean.lua
index ba38736e8a..a2ac170f20 100644
--- a/src/frontends/lua/lean.lua
+++ b/src/frontends/lua/lean.lua
@@ -1,4 +1,4 @@
-static char const * g_leanlua_extra = R"Lua(
+static char const * g_extra_code = R"Lua(
 function Consts(s)
   r = {}
   i = 1
diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp
new file mode 100644
index 0000000000..01facf0c1d
--- /dev/null
+++ b/src/frontends/lua/register_modules.cpp
@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/script_state.h"
+#include "util/numerics/register_module.h"
+#include "util/sexpr/register_module.h"
+#include "library/kernel_bindings.h"
+#include "library/arith/register_module.h"
+#include "library/tactic/register_module.h"
+#include "frontends/lean/register_module.h"
+#include "frontends/lua/lean.lua"
+
+namespace lean {
+void register_modules() {
+    register_numerics_module();
+    register_sexpr_module();
+    register_kernel_module();
+    register_arith_module();
+    register_tactic_module();
+    register_frontend_lean_module();
+    script_state::register_code(g_extra_code);
+}
+}
diff --git a/src/util/open_module.h b/src/frontends/lua/register_modules.h
similarity index 50%
rename from src/util/open_module.h
rename to src/frontends/lua/register_modules.h
index bf416845d0..5a9355174a 100644
--- a/src/util/open_module.h
+++ b/src/frontends/lua/register_modules.h
@@ -5,14 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "util/exception.h"
-#include "util/name.h"
-#include "util/splay_map.h"
-
 namespace lean {
-inline void open_util_module(lua_State * L) {
-    open_exception(L);
-    open_name(L);
-    open_splay_map(L);
-}
+/**
+   \brief Register all modules at \c script_state.
+*/
+void register_modules();
 }
diff --git a/src/library/arith/open_module.h b/src/library/arith/register_module.h
similarity index 75%
rename from src/library/arith/open_module.h
rename to src/library/arith/register_module.h
index a68879fe38..c68d9b7058 100644
--- a/src/library/arith/open_module.h
+++ b/src/library/arith/register_module.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/script_state.h"
 #include "library/arith/nat.h"
 #include "library/arith/int.h"
 #include "library/arith/real.h"
@@ -15,4 +16,7 @@ inline void open_arith_module(lua_State * L) {
     open_int(L);
     open_real(L);
 }
+inline void register_arith_module() {
+    script_state::register_module(open_arith_module);
+}
 }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 9326ba4089..2b45154546 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <utility>
-#include "util/lua.h"
 #include "util/sstream.h"
+#include "util/script_state.h"
 #include "kernel/expr.h"
 #include "kernel/context.h"
 #include "kernel/formatter.h"
@@ -1560,7 +1560,6 @@ static void open_metavar_env(lua_State * L) {
     SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars");
 }
 
-
 void open_kernel_module(lua_State * L) {
     open_level(L);
     open_local_context(L);
@@ -1574,4 +1573,8 @@ void open_kernel_module(lua_State * L) {
     open_io_state(L);
     open_type_inferer(L);
 }
+
+void register_kernel_module() {
+    script_state::register_module(open_kernel_module);
+}
 }
diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h
index e3e018387c..6879563f9d 100644
--- a/src/library/kernel_bindings.h
+++ b/src/library/kernel_bindings.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 void open_kernel_module(lua_State * L);
+void register_kernel_module();
 UDATA_DEFS(level)
 UDATA_DEFS(local_entry)
 UDATA_DEFS_CORE(local_context)
diff --git a/src/library/script_evaluator.h b/src/library/script_evaluator.h
deleted file mode 100644
index 4d917b3e62..0000000000
--- a/src/library/script_evaluator.h
+++ /dev/null
@@ -1,24 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/script_exception.h"
-
-namespace lean {
-class environment;
-class io_state;
-/**
-   \brief Abstract base class for script code evaluators.
-   These evaluators are used to execute user-supplied code embedded in frontend files (.e.g., .lean, .smt2, etc).
-   In the current implementation we only have one implementation of this class based on the Lua programming language. So, the main purpose of this class is to organize the dependencies between modules.
-*/
-class script_evaluator {
-public:
-    virtual ~script_evaluator() {}
-    virtual void dostring(char const * str) = 0;
-    virtual void dostring(char const * str, environment & env, io_state & st) = 0;
-};
-}
diff --git a/src/library/tactic/open_module.h b/src/library/tactic/register_module.h
similarity index 79%
rename from src/library/tactic/open_module.h
rename to src/library/tactic/register_module.h
index 4f0bb700f9..9e1eb0e33d 100644
--- a/src/library/tactic/open_module.h
+++ b/src/library/tactic/register_module.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/script_state.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/cex_builder.h"
@@ -17,4 +18,7 @@ inline void open_tactic_module(lua_State * L) {
     open_cex_builder(L);
     open_proof_state(L);
 }
+inline void register_tactic_module() {
+    script_state::register_module(open_tactic_module);
+}
 }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index afb40579d0..1d76d67607 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -10,16 +10,17 @@ Author: Leonardo de Moura
 #include <getopt.h>
 #include "util/debug.h"
 #include "util/interrupt.h"
+#include "util/script_state.h"
 #include "kernel/printer.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/frontend.h"
-#include "frontends/lua/leanlua_state.h"
+#include "frontends/lua/register_modules.h"
 #include "version.h"
 
 using lean::shell;
 using lean::frontend;
 using lean::parser;
-using lean::leanlua_state;
+using lean::script_state;
 using lean::unreachable_reached;
 using lean::invoke_debugger;
 using lean::notify_assertion_violation;
@@ -67,6 +68,7 @@ static struct option g_long_options[] = {
 };
 
 int main(int argc, char ** argv) {
+    lean::register_modules();
     input_kind default_k = input_kind::Lean; // default
     int optind     = 1;
     while (true) {
@@ -93,7 +95,7 @@ int main(int argc, char ** argv) {
         }
     }
     frontend f;
-    leanlua_state S;
+    script_state S;
     if (optind >= argc) {
         display_header(std::cout);
         std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index c5f6775c71..17fe157ca7 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,7 +1,7 @@
 add_library(util trace.cpp debug.cpp name.cpp exception.cpp
   interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp
   ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp
-  script_exception.cpp splay_map.cpp lua.cpp luaref.cpp
-  lua_exception.cpp)
+  script_state.cpp script_exception.cpp splay_map.cpp lua.cpp
+  luaref.cpp)
 
 target_link_libraries(util ${LEAN_LIBS})
diff --git a/src/util/lua.cpp b/src/util/lua.cpp
index e68c25959f..9468fc7df5 100644
--- a/src/util/lua.cpp
+++ b/src/util/lua.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <memory>
 #include "util/lua.h"
-#include "util/lua_exception.h"
+#include "util/script_exception.h"
 #include "util/debug.h"
 
 namespace lean {
@@ -94,7 +94,7 @@ void check_result(lua_State * L, int result) {
         if (is_exception(L, -1))
             to_exception(L, -1).rethrow();
         else
-            throw lua_exception(lua_tostring(L, -1));
+            throw script_exception(lua_tostring(L, -1));
     }
 }
 
@@ -122,7 +122,7 @@ void pcall(lua_State * L, int nargs, int nresults, int errorfun) {
 int safe_function_wrapper(lua_State * L, lua_CFunction f) {
     try {
         return f(L);
-    } catch (lua_exception & e) {
+    } catch (script_exception & e) {
         lua_pushstring(L, e.what());
     } catch (exception & e) {
         push_exception(L, e);
diff --git a/src/util/lua_exception.cpp b/src/util/lua_exception.cpp
deleted file mode 100644
index cda3b762a5..0000000000
--- a/src/util/lua_exception.cpp
+++ /dev/null
@@ -1,71 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <sstream>
-#include <string>
-#include <cstdlib>
-#include "util/debug.h"
-#include "util/lua_exception.h"
-
-namespace lean {
-lua_exception::lua_exception(char const * lua_error):script_exception() {
-    lean_assert(lua_error);
-    std::string fname;
-    std::string line;
-    std::string msg;
-    int state = 0;
-    char const * it = lua_error;
-    while (*it) {
-        if (state == 0) {
-            if (*it == ':') {
-                state = 1;
-            } else {
-                fname += *it;
-            }
-        } else if (state == 1) {
-            if (*it == ':') {
-                state = 2;
-            } else {
-                line += *it;
-            }
-        } else {
-            msg += *it;
-        }
-        it++;
-    }
-    if (state != 2) {
-        // failed to decode Lua error message
-        m_source = source::Unknown;
-        m_msg = lua_error;
-    } else {
-        if (fname == "[string \"...\"]") {
-            m_source = source::String;
-        } else {
-            m_source = source::File;
-            m_file   = fname;
-        }
-        m_line   = atoi(line.c_str());
-        m_msg = msg;
-    }
-}
-
-lua_exception::~lua_exception() {
-}
-
-char const * lua_exception::get_filename() const {
-    lean_assert(get_source() == source::File);
-    return m_file.c_str();
-}
-
-unsigned lua_exception::get_line() const {
-    lean_assert(get_source() != source::Unknown);
-    return m_line;
-}
-
-char const * lua_exception::get_msg() const noexcept {
-    return exception::what();
-}
-}
diff --git a/src/util/lua_exception.h b/src/util/lua_exception.h
deleted file mode 100644
index 6877bc54eb..0000000000
--- a/src/util/lua_exception.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <string>
-#include "util/exception.h"
-#include "util/script_exception.h"
-
-namespace lean {
-/**
-   \brief Exception for wrapping errors produced by the Lua engine.
-*/
-class lua_exception : public script_exception {
-private:
-    source      m_source;
-    std::string m_file;   // if source == File, then this field contains the filename that triggered the error.
-    unsigned    m_line;   // line number
-    lua_exception(source s, std::string f, unsigned l):m_source(s), m_file(f), m_line(l) {}
-public:
-    lua_exception(char const * lua_error);
-    virtual ~lua_exception();
-    virtual source get_source() const { return m_source; }
-    virtual char const * get_filename() const;
-    virtual unsigned get_line() const;
-    /** \brief Return error message without position information */
-    virtual char const * get_msg() const noexcept;
-    virtual exception * clone() const { return new lua_exception(m_source, m_file, m_line); }
-    virtual void rethrow() const { throw *this; }
-};
-}
diff --git a/src/util/numerics/open_module.h b/src/util/numerics/register_module.h
similarity index 72%
rename from src/util/numerics/open_module.h
rename to src/util/numerics/register_module.h
index 2ca1660361..bd265855f1 100644
--- a/src/util/numerics/open_module.h
+++ b/src/util/numerics/register_module.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/script_state.h"
 #include "util/numerics/mpz.h"
 #include "util/numerics/mpq.h"
 
@@ -13,4 +14,7 @@ inline void open_numerics_module(lua_State * L) {
     open_mpz(L);
     open_mpq(L);
 }
+inline void register_numerics_module() {
+    script_state::register_module(open_numerics_module);
+}
 }
diff --git a/src/util/script_exception.cpp b/src/util/script_exception.cpp
index 9accf6e3d4..66f7a348fa 100644
--- a/src/util/script_exception.cpp
+++ b/src/util/script_exception.cpp
@@ -6,9 +6,68 @@ Author: Leonardo de Moura
 */
 #include <sstream>
 #include <string>
+#include "util/debug.h"
 #include "util/script_exception.h"
 
 namespace lean {
+script_exception::script_exception(char const * lua_error) {
+    lean_assert(lua_error);
+    std::string fname;
+    std::string line;
+    std::string msg;
+    int state = 0;
+    char const * it = lua_error;
+    while (*it) {
+        if (state == 0) {
+            if (*it == ':') {
+                state = 1;
+            } else {
+                fname += *it;
+            }
+        } else if (state == 1) {
+            if (*it == ':') {
+                state = 2;
+            } else {
+                line += *it;
+            }
+        } else {
+            msg += *it;
+        }
+        it++;
+    }
+    if (state != 2) {
+        // failed to decode Lua error message
+        m_source = source::Unknown;
+        m_msg = lua_error;
+    } else {
+        if (fname == "[string \"...\"]") {
+            m_source = source::String;
+        } else {
+            m_source = source::File;
+            m_file   = fname;
+        }
+        m_line   = atoi(line.c_str());
+        m_msg = msg;
+    }
+}
+
+script_exception::~script_exception() {
+}
+
+char const * script_exception::get_filename() const {
+    lean_assert(get_source() == source::File);
+    return m_file.c_str();
+}
+
+unsigned script_exception::get_line() const {
+    lean_assert(get_source() != source::Unknown);
+    return m_line;
+}
+
+char const * script_exception::get_msg() const noexcept {
+    return exception::what();
+}
+
 char const * script_exception::what() const noexcept {
     static thread_local std::string buffer;
     std::ostringstream strm;
diff --git a/src/util/script_exception.h b/src/util/script_exception.h
index d1e65a9c8d..073fcf7ac6 100644
--- a/src/util/script_exception.h
+++ b/src/util/script_exception.h
@@ -5,19 +5,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <string>
 #include "util/exception.h"
 
 namespace lean {
 /**
-   \brief Base class for exceptions producing when evaluating scripts.
+   \brief Exception for wrapping errors produced by the Lua engine.
 */
 class script_exception : public exception {
 public:
     enum class source { String, File, Unknown };
-    virtual source get_source() const = 0;
-    virtual char const * get_filename() const = 0;
-    virtual unsigned get_line() const = 0;
-    virtual char const * get_msg() const noexcept = 0;
+private:
+    source      m_source;
+    std::string m_file;   // if source == File, then this field contains the filename that triggered the error.
+    unsigned    m_line;   // line number
+    script_exception(source s, std::string f, unsigned l):m_source(s), m_file(f), m_line(l) {}
+public:
+    script_exception(char const * lua_error);
+    virtual ~script_exception();
     virtual char const * what() const noexcept;
+    virtual source get_source() const { return m_source; }
+    virtual char const * get_filename() const;
+    virtual unsigned get_line() const;
+    /** \brief Return error message without position information */
+    virtual char const * get_msg() const noexcept;
+    virtual exception * clone() const { return new script_exception(m_source, m_file, m_line); }
+    virtual void rethrow() const { throw *this; }
 };
 }
diff --git a/src/frontends/lua/leanlua_state.cpp b/src/util/script_state.cpp
similarity index 86%
rename from src/frontends/lua/leanlua_state.cpp
rename to src/util/script_state.cpp
index f07ae51e1e..28dff8d4bc 100644
--- a/src/frontends/lua/leanlua_state.cpp
+++ b/src/util/script_state.cpp
@@ -9,31 +9,38 @@ Author: Leonardo de Moura
 #include <thread>
 #include <chrono>
 #include <string>
+#include <vector>
+#include <condition_variable>
 #include "util/lua.h"
 #include "util/debug.h"
 #include "util/exception.h"
 #include "util/memory.h"
 #include "util/buffer.h"
 #include "util/interrupt.h"
-#include "util/open_module.h"
-#include "util/numerics/open_module.h"
-#include "util/sexpr/open_module.h"
-#include "library/kernel_bindings.h"
-#include "library/arith/open_module.h"
-#include "library/tactic/open_module.h"
-#include "frontends/lean/frontend.h"
-#include "frontends/lua/leanlua_state.h"
-#include "frontends/lua/frontend_lean.h"
-#include "frontends/lua/lean.lua"
+#include "util/script_state.h"
+#include "util/script_exception.h"
+#include "util/name.h"
+#include "util/splay_map.h"
 
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
 
 namespace lean {
+static std::vector<script_state::reg_fn> g_modules;
+static std::vector<char const *> g_code;
+
+void script_state::register_module(reg_fn f) {
+    g_modules.push_back(f);
+}
+
+void script_state::register_code(char const * code) {
+    g_code.push_back(code);
+}
+
 void open_extra(lua_State * L);
 
 static char g_weak_ptr_key; // key for Lua registry (used at get_weak_ptr and save_weak_ptr)
 
-struct leanlua_state::imp {
+struct script_state::imp {
     lua_State *           m_state;
     std::recursive_mutex  m_mutex;
 
@@ -63,16 +70,18 @@ struct leanlua_state::imp {
         if (m_state == nullptr)
             throw exception("fail to create Lua interpreter");
         luaL_openlibs(m_state);
-        open_util_module(m_state);
-        open_numerics_module(m_state);
-        open_sexpr_module(m_state);
-        open_kernel_module(m_state);
-        open_arith_module(m_state);
-        open_tactic_module(m_state);
-        open_frontend_lean(m_state);
+        open_exception(m_state);
+        open_name(m_state);
+        open_splay_map(m_state);
         open_extra(m_state);
 
-        dostring(g_leanlua_extra);
+        for (auto f : g_modules) {
+            f(m_state);
+        }
+
+        for (auto c : g_code) {
+            dostring(c);
+        }
     }
 
     ~imp() {
@@ -91,47 +100,37 @@ struct leanlua_state::imp {
         std::lock_guard<std::recursive_mutex> lock(m_mutex);
         ::lean::dostring(m_state, str);
     }
-
-    void dostring(char const * str, environment & env, io_state & st) {
-        set_io_state    set1(m_state, st);
-        set_environment set2(m_state, env);
-        dostring(str);
-    }
 };
 
-leanlua_state to_leanlua_state(lua_State * L) {
-    return leanlua_state(*leanlua_state::imp::get_weak_ptr(L));
+script_state to_script_state(lua_State * L) {
+    return script_state(*script_state::imp::get_weak_ptr(L));
 }
 
-leanlua_state::leanlua_state():
+script_state::script_state():
     m_ptr(new imp()) {
     m_ptr->save_weak_ptr(m_ptr);
 }
 
-leanlua_state::leanlua_state(std::weak_ptr<imp> const & ptr):m_ptr(ptr.lock()) {
+script_state::script_state(std::weak_ptr<imp> const & ptr):m_ptr(ptr.lock()) {
     lean_assert(m_ptr);
 }
 
-leanlua_state::~leanlua_state() {
+script_state::~script_state() {
 }
 
-void leanlua_state::dofile(char const * fname) {
+void script_state::dofile(char const * fname) {
     m_ptr->dofile(fname);
 }
 
-void leanlua_state::dostring(char const * str) {
+void script_state::dostring(char const * str) {
     m_ptr->dostring(str);
 }
 
-void leanlua_state::dostring(char const * str, environment & env, io_state & st) {
-    m_ptr->dostring(str, env, st);
-}
-
-std::recursive_mutex & leanlua_state::get_mutex() {
+std::recursive_mutex & script_state::get_mutex() {
     return m_ptr->m_mutex;
 }
 
-lua_State * leanlua_state::get_state() {
+lua_State * script_state::get_state() {
     return m_ptr->m_state;
 }
 
@@ -141,25 +140,25 @@ bool is_state(lua_State * L, int idx) {
     return testudata(L, idx, state_mt);
 }
 
-leanlua_state & to_state(lua_State * L, int idx) {
-    return *static_cast<leanlua_state*>(luaL_checkudata(L, idx, state_mt));
+script_state & to_state(lua_State * L, int idx) {
+    return *static_cast<script_state*>(luaL_checkudata(L, idx, state_mt));
 }
 
-int push_state(lua_State * L, leanlua_state const & s) {
-    void * mem = lua_newuserdata(L, sizeof(leanlua_state));
-    new (mem) leanlua_state(s);
+int push_state(lua_State * L, script_state const & s) {
+    void * mem = lua_newuserdata(L, sizeof(script_state));
+    new (mem) script_state(s);
     luaL_getmetatable(L, state_mt);
     lua_setmetatable(L, -2);
     return 1;
 }
 
 static int mk_state(lua_State * L) {
-    leanlua_state r;
+    script_state r;
     return push_state(L, r);
 }
 
 static int state_gc(lua_State * L) {
-    to_state(L, 1).~leanlua_state();
+    to_state(L, 1).~script_state();
     return 0;
 }
 
@@ -237,7 +236,7 @@ int state_dostring(lua_State * L) {
             int sz_before = lua_gettop(S);
             int status = luaL_loadstring(S, script);
             if (status)
-                throw lua_exception(lua_tostring(S, -1));
+                throw script_exception(lua_tostring(S, -1));
 
             copy_values(L, first, last, S);
 
@@ -296,7 +295,7 @@ class data_channel {
     // We use a lua_State to implement the channel. This is quite hackish,
     // but it is a convenient storage for Lua objects sent from one state to
     // another.
-    leanlua_state           m_channel;
+    script_state            m_channel;
     int                     m_ini;
     std::mutex              m_mutex;
     std::condition_variable m_cv;
@@ -390,14 +389,14 @@ int channel_write(lua_State * L) {
 }
 
 class leanlua_thread {
-    leanlua_state                   m_state;
+    script_state                    m_state;
     int                             m_sz_before;
     std::unique_ptr<exception>      m_exception;
     std::atomic<data_channel_ref *> m_in_channel_addr;
     std::atomic<data_channel_ref *> m_out_channel_addr;
     interruptible_thread            m_thread;
 public:
-    leanlua_thread(leanlua_state const & st, int sz_before, int num_args):
+    leanlua_thread(script_state const & st, int sz_before, int num_args):
         m_state(st),
         m_sz_before(sz_before),
         m_in_channel_addr(0),
@@ -411,7 +410,7 @@ public:
                             if (is_exception(S, -1))
                                 m_exception.reset(to_exception(S, -1).clone());
                             else
-                                m_exception.reset(new lua_exception(lua_tostring(S, -1)));
+                                m_exception.reset(new script_exception(lua_tostring(S, -1)));
                         }
                     });
             }) {
@@ -476,7 +475,7 @@ leanlua_thread & to_thread(lua_State * L, int idx) {
 
 int mk_thread(lua_State * L) {
     check_threadsafe();
-    leanlua_state & st  = to_state(L, 1);
+    script_state & st   = to_state(L, 1);
     char const * script = luaL_checkstring(L, 2);
     int first           = 3;
     int last            = lua_gettop(L);
@@ -486,7 +485,7 @@ int mk_thread(lua_State * L) {
             sz_before = lua_gettop(S);
             int result  = luaL_loadstring(S, script);
             if (result)
-                throw lua_exception(lua_tostring(S, -1));
+                throw script_exception(lua_tostring(S, -1));
             copy_values(L, first, last, S);
         });
     void * mem = lua_newuserdata(L, sizeof(leanlua_thread));
@@ -560,15 +559,9 @@ static void open_interrupt(lua_State * L) {
     SET_GLOBAL_FUN(channel_write,     "write");
 }
 
-static int mk_environment(lua_State * L) {
-    frontend f;
-    return push_environment(L, f.get_environment());
-}
-
 void open_extra(lua_State * L) {
     open_state(L);
     open_thread(L);
     open_interrupt(L);
-    SET_GLOBAL_FUN(mk_environment,  "environment");
 }
 }
diff --git a/src/frontends/lua/leanlua_state.h b/src/util/script_state.h
similarity index 64%
rename from src/frontends/lua/leanlua_state.h
rename to src/util/script_state.h
index 7c877ba226..b41cabf786 100644
--- a/src/frontends/lua/leanlua_state.h
+++ b/src/util/script_state.h
@@ -8,27 +8,23 @@ Author: Leonardo de Moura
 #include <memory>
 #include <mutex>
 #include <lua.hpp>
-#include "util/lua_exception.h"
-#include "library/script_evaluator.h"
 
 namespace lean {
-class environment;
-class io_state;
 /**
    \brief Wrapper for lua_State objects which contains all Lean bindings.
 */
-class leanlua_state : public script_evaluator {
+class script_state {
 public:
     struct imp;
 private:
     std::shared_ptr<imp> m_ptr;
-    leanlua_state(std::weak_ptr<imp> const & ptr);
-    friend leanlua_state to_leanlua_state(lua_State * L);
+    script_state(std::weak_ptr<imp> const & ptr);
+    friend script_state to_script_state(lua_State * L);
     std::recursive_mutex & get_mutex();
     lua_State * get_state();
 public:
-    leanlua_state();
-    virtual ~leanlua_state();
+    script_state();
+    virtual ~script_state();
 
     /**
        \brief Execute the file with the given name.
@@ -41,13 +37,6 @@ public:
     */
     virtual void dostring(char const * str);
 
-    /**
-       \brief Execute the given script, but sets the registry with the given environment object.
-       The registry can be accessed by \str by invoking the function <tt>env()</tt>.
-       The script \c str should not store a reference to the environment \c env.
-    */
-    virtual void dostring(char const * str, environment & env, io_state & st);
-
     /**
        \brief Execute \c f in the using the internal Lua State.
     */
@@ -68,9 +57,14 @@ public:
     typename std::result_of<F(lua_State * L)>::type unguarded_apply(F && f) {
         return f(get_state());
     }
+
+    typedef void (*reg_fn)(lua_State *); // NOLINT
+    static void register_module(reg_fn f);
+
+    static void register_code(char const * code);
 };
 /**
-   \brief Return a reference to the leanlua_state object that is wrapping \c L.
+   \brief Return a reference to the script_state object that is wrapping \c L.
 */
-leanlua_state to_leanlua_state(lua_State * L);
+script_state to_script_state(lua_State * L);
 }
diff --git a/src/util/sexpr/open_module.h b/src/util/sexpr/register_module.h
similarity index 76%
rename from src/util/sexpr/open_module.h
rename to src/util/sexpr/register_module.h
index b341f5b25d..cc1656290b 100644
--- a/src/util/sexpr/open_module.h
+++ b/src/util/sexpr/register_module.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/script_state.h"
 #include "util/sexpr/sexpr.h"
 #include "util/sexpr/options.h"
 #include "util/sexpr/format.h"
@@ -15,4 +16,7 @@ inline void open_sexpr_module(lua_State * L) {
     open_options(L);
     open_format(L);
 }
+inline void register_sexpr_module() {
+    script_state::register_module(open_sexpr_module);
+}
 }