From b08c60669646b26edbcdc59e2576851fcd8bf630 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Dec 2013 16:39:37 -0800
Subject: [PATCH] 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>
---
 src/library/io_state.cpp           |  2 ++
 tests/lean/lua17.lean              | 14 ++++++++++++++
 tests/lean/lua17.lean.expected.out | 13 +++++++++++++
 3 files changed, 29 insertions(+)
 create mode 100644 tests/lean/lua17.lean
 create mode 100644 tests/lean/lua17.lean.expected.out

diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp
index 89123361c..7fbe2d58b 100644
--- a/src/library/io_state.cpp
+++ b/src/library/io_state.cpp
@@ -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) {
diff --git a/tests/lean/lua17.lean b/tests/lean/lua17.lean
new file mode 100644
index 000000000..d0c9c61d0
--- /dev/null
+++ b/tests/lean/lua17.lean
@@ -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
\ No newline at end of file
diff --git a/tests/lean/lua17.lean.expected.out b/tests/lean/lua17.lean.expected.out
new file mode 100644
index 000000000..10c8b08d4
--- /dev/null
+++ b/tests/lean/lua17.lean.expected.out
@@ -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 : ℤ