fix(library/io_state): bug in the io_state Lua bindings
This commit also includes a new test that exposes the problem. The options in the io_state object were being lost. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
2648f41eaa
commit
b08c606696
3 changed files with 29 additions and 0 deletions
|
@ -194,6 +194,8 @@ set_io_state::~set_io_state() {
|
|||
lua_settable(m_state, LUA_REGISTRYINDEX);
|
||||
if (!m_prev)
|
||||
set_global_options(m_state, m_prev_options);
|
||||
else
|
||||
set_global_options(m_state, m_prev->get_options());
|
||||
}
|
||||
|
||||
io_state * get_io_state(lua_State * L) {
|
||||
|
|
14
tests/lean/lua17.lean
Normal file
14
tests/lean/lua17.lean
Normal file
|
@ -0,0 +1,14 @@
|
|||
|
||||
Variables a b : Int
|
||||
Show Options
|
||||
(**
|
||||
local ios = io_state()
|
||||
|
||||
print(get_options())
|
||||
print(get_options())
|
||||
ios:print(parse_lean("a + b"))
|
||||
print(parse_lean("fun x, a + x"))
|
||||
print(get_options())
|
||||
**)
|
||||
Show Options
|
||||
Show Environment 2
|
13
tests/lean/lua17.lean.expected.out
Normal file
13
tests/lean/lua17.lean.expected.out
Normal file
|
@ -0,0 +1,13 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Assumed: a
|
||||
Assumed: b
|
||||
⟨pp::unicode ↦ true, pp::colors ↦ false⟩
|
||||
⟨pp::unicode ↦ true, pp::colors ↦ false⟩
|
||||
⟨pp::unicode ↦ true, pp::colors ↦ false⟩
|
||||
Int::add a b
|
||||
λ x : ℤ, a + x
|
||||
⟨pp::unicode ↦ true, pp::colors ↦ false⟩
|
||||
⟨pp::unicode ↦ true, pp::colors ↦ false⟩
|
||||
Variable a : ℤ
|
||||
Variable b : ℤ
|
Loading…
Reference in a new issue