From 35bacf95fc7cd80dd75b3e2ac255962bd142664b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Jan 2014 18:21:14 -0800 Subject: [PATCH] feat(shell): provide the default environment when parsing Lua files Signed-off-by: Leonardo de Moura --- src/frontends/lean/register_module.cpp | 1 + src/shell/lean.cpp | 8 +++++++- tests/lua/env4.lua | 1 - 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp index d912b24b8..35b3d0aaf 100644 --- a/src/frontends/lean/register_module.cpp +++ b/src/frontends/lean/register_module.cpp @@ -94,6 +94,7 @@ static void parse_lean_cmds_core(lua_State * L, rw_shared_environment const & en set_global_options(L, s.get_options()); } else { parse_lean_cmds_core(L, env, *io); + set_global_options(L, io->get_options()); } } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 28b8263a7..d416f1656 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -227,7 +227,13 @@ int main(int argc, char ** argv) { } } else if (k == input_kind::Lua) { try { - S.dofile(argv[i]); + S.apply([&](lua_State * L) { + lean::set_io_state set1(L, ios); + lean::set_environment set2(L, env); + S.exec_unprotected([&]() { + S.dofile(argv[i]); + }); + }); } catch (lean::exception & ex) { std::cerr << ex.what() << std::endl; ok = false; diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index 7ae5fe8ce..ba12b6823 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -1,4 +1,3 @@ -assert(not pcall(function() get_environment() end)) local env = environment() env:import("Int") env:add_uvar_cnstr("M", level(level(), 1))