From c7e9e238ec7b1a7d8ab0ca4cfc5815096b656469 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Aug 2014 10:46:49 -0700
Subject: [PATCH] fix(frontends/lean/server): ignore output produced by worker
 thread, fixes #98

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/server.cpp                 | 26 ++++++-------------
 src/library/io_state.cpp                      |  6 +++++
 src/library/io_state.h                        |  1 +
 tests/lean/interactive/in1.input.expected.out |  2 --
 tests/lean/interactive/t4.input.expected.out  |  1 -
 5 files changed, 15 insertions(+), 21 deletions(-)

diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index c71dd9377..d6077be55 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -117,19 +117,6 @@ static std::string & trim(std::string & s) {
     return ltrim(rtrim(s));
 }
 
-struct scoped_updt_options {
-    io_state & m_ios;
-    options    m_old_options;
-public:
-    scoped_updt_options(io_state & ios, options const & opts):
-        m_ios(ios), m_old_options(m_ios.get_options()) {
-        m_ios.set_options(join(opts, m_old_options));
-    }
-    ~scoped_updt_options() {
-        m_ios.set_options(m_old_options);
-    }
-};
-
 void server::process_from(unsigned linenum) {
     reset_thread();
     unsigned i = m_file->find(linenum);
@@ -145,8 +132,11 @@ void server::process_from(unsigned linenum) {
                 try {
                     snapshot & s = i == 0 ? m_empty_snapshot : m_file->m_snapshots[i-1];
                     std::istringstream strm(block);
-                    scoped_updt_options updt(m_ios, s.m_options);
-                    parser p(s.m_env, m_ios, strm, m_file->m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
+                    std::shared_ptr<output_channel> out1(new string_output_channel());
+                    std::shared_ptr<output_channel> out2(new string_output_channel());
+                    io_state ios(m_ios, out1, out2);
+                    ios.set_options(s.m_options);
+                    parser p(s.m_env, ios, strm, m_file->m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
                              &m_file->m_snapshots, &m_file->m_info);
                     p.set_cache(&m_cache);
                     p();
@@ -264,10 +254,10 @@ void server::show_info(unsigned linenum) {
 
 void server::eval_core(environment const & env, options const & o, std::string const & line) {
     std::istringstream strm(line);
-    scoped_updt_options updt(m_ios, o);
+    io_state ios(m_ios, o);
     m_out << "-- BEGINEVAL" << std::endl;
     try {
-        parser p(env, m_ios, strm, "EVAL_command", true);
+        parser p(env, ios, strm, "EVAL_command", true);
         p();
     } catch (exception & ex) {
         m_out << ex.what() << std::endl;
@@ -279,7 +269,7 @@ void server::eval(std::string const & line) {
     if (!m_file) {
         eval_core(m_env, m_ios.get_options(), line);
     } else if (auto p = m_file->m_info.get_final_env_opts()) {
-        eval_core(p->first, p->second, line);
+        eval_core(p->first, join(p->second, m_ios.get_options()), line);
     } else {
         eval_core(m_env, m_ios.get_options(), line);
     }
diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp
index 83c6068af..bc9a85fa2 100644
--- a/src/library/io_state.cpp
+++ b/src/library/io_state.cpp
@@ -32,6 +32,12 @@ io_state::io_state(io_state const & ios, std::shared_ptr<output_channel> const &
     m_regular_channel(r),
     m_diagnostic_channel(d) {
 }
+io_state::io_state(io_state const & ios, options const & o):
+    m_options(o),
+    m_formatter_factory(ios.m_formatter_factory),
+    m_regular_channel(ios.m_regular_channel),
+    m_diagnostic_channel(ios.m_diagnostic_channel) {
+}
 
 io_state::~io_state() {}
 
diff --git a/src/library/io_state.h b/src/library/io_state.h
index c9f42149a..6a53b4a90 100644
--- a/src/library/io_state.h
+++ b/src/library/io_state.h
@@ -26,6 +26,7 @@ public:
     io_state(formatter_factory const & fmtf);
     io_state(options const & opts, formatter_factory const & fmtf);
     io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const d);
+    io_state(io_state const & ios, options const & o);
     ~io_state();
 
     options get_options() const { return m_options; }
diff --git a/tests/lean/interactive/in1.input.expected.out b/tests/lean/interactive/in1.input.expected.out
index c650f51f0..25318909a 100644
--- a/tests/lean/interactive/in1.input.expected.out
+++ b/tests/lean/interactive/in1.input.expected.out
@@ -90,8 +90,6 @@ B
 b
 -- ACK
 -- ENDINFO
-simple.lean:4:0: error: command expected
-simple.lean:5:37: error: unknown identifier 'foo'
 -- BEGININFO
 -- SYMBOL|4|22
 Type
diff --git a/tests/lean/interactive/t4.input.expected.out b/tests/lean/interactive/t4.input.expected.out
index 2abf61185..3538a731b 100644
--- a/tests/lean/interactive/t4.input.expected.out
+++ b/tests/lean/interactive/t4.input.expected.out
@@ -1,4 +1,3 @@
-epsilon (λ (x : nat), true) : nat
 -- BEGININFO
 -- TYPE|6|6
 (nat → Prop) → nat