From 373bda0c741d1d43542e1bbfa8ea6ffb6bed01e2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Aug 2014 18:12:22 -0700 Subject: [PATCH] fix(frontends/lean/server): in valid line tracking, add 'VALID' command similar to show, but marks invalid lines with a '*' Signed-off-by: Leonardo de Moura --- src/frontends/lean/info_manager.cpp | 16 ++++++++++++++-- src/frontends/lean/info_manager.h | 1 + src/frontends/lean/server.cpp | 24 ++++++++++++++++++------ src/frontends/lean/server.h | 4 ++-- 4 files changed, 35 insertions(+), 10 deletions(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 9366ea372..374b55428 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -229,7 +229,7 @@ struct info_manager::imp { lean_assert(l > 0); if (l >= m_line_data.size()) { m_line_data.resize(l+1); - m_line_valid.resize(l+1, true); + m_line_valid.resize(l+1, false); } } @@ -337,10 +337,12 @@ struct info_manager::imp { void insert_line(unsigned l) { lock_guard lc(m_mutex); + lean_assert(m_line_data.size() == m_line_valid.size()); synch_line(l); if (m_processed_upto > l - 1) m_processed_upto = l - 1; m_line_data.push_back(info_data_set()); + m_line_valid.push_back(false); unsigned i = m_line_data.size(); while (i > l) { --i; @@ -352,6 +354,7 @@ struct info_manager::imp { void remove_line(unsigned l) { lock_guard lc(m_mutex); + lean_assert(m_line_data.size() == m_line_valid.size()); lean_assert(l > 0); if (l >= m_line_data.size()) return; @@ -361,12 +364,14 @@ struct info_manager::imp { m_line_valid[i] = m_line_valid[i+1]; } m_line_data.pop_back(); + m_line_valid.pop_back(); if (m_processed_upto > l - 1) m_processed_upto = l - 1; } void invalidate_line_col_core(unsigned l, optional const & c) { lock_guard lc(m_mutex); + lean_assert(m_line_data.size() == m_line_valid.size()); synch_line(l); if (m_processed_upto > l - 1) m_processed_upto = l - 1; @@ -391,6 +396,11 @@ struct info_manager::imp { invalidate_line_col_core(l, optional(c)); } + void set_processed_upto(unsigned l) { + lock_guard lc(m_mutex); + m_processed_upto = l; + } + void commit_upto(unsigned l, bool valid) { lock_guard lc(m_mutex); if (m_block_new_info) @@ -402,8 +412,9 @@ struct info_manager::imp { bool is_invalidated(unsigned l) { lock_guard lc(m_mutex); + lean_assert(m_line_data.size() == m_line_valid.size()); if (l >= m_line_valid.size()) - return false; + return true; return !m_line_valid[l]; } @@ -481,6 +492,7 @@ void info_manager::remove_line(unsigned l) { m_ptr->remove_line(l); } void info_manager::invalidate_line(unsigned l) { m_ptr->invalidate_line(l); } void info_manager::invalidate_line_col(unsigned l, unsigned c) { m_ptr->invalidate_line_col(l, c); } void info_manager::commit_upto(unsigned l, bool valid) { m_ptr->commit_upto(l, valid); } +void info_manager::set_processed_upto(unsigned l) { m_ptr->set_processed_upto(l); } bool info_manager::is_invalidated(unsigned l) const { return m_ptr->is_invalidated(l); } void info_manager::save_environment_options(unsigned l, environment const & env, options const & o) { m_ptr->save_environment_options(l, env, o); diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index d5720db47..511933424 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -31,6 +31,7 @@ public: void invalidate_line(unsigned l); void invalidate_line_col(unsigned l, unsigned c); void commit_upto(unsigned l, bool valid); + void set_processed_upto(unsigned l); bool is_invalidated(unsigned l) const; void save_environment_options(unsigned l, environment const & env, options const & o); optional> get_final_env_opts() const; diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 06e6c5aca..23a9c9b89 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -68,10 +68,18 @@ void server::file::remove_line(unsigned linenum) { m_lines.pop_back(); } -void server::file::show(std::ostream & out) { +void server::file::show(std::ostream & out, bool valid) { lock_guard lk(m_lines_mutex); - for (unsigned i = 0; i < m_lines.size(); i++) + for (unsigned i = 0; i < m_lines.size(); i++) { + if (valid) { + if (m_info.is_invalidated(i+1)) + out << "*"; + else + out << " "; + out << " "; + } out << m_lines[i] << "\n"; + } } /** @@ -144,11 +152,12 @@ server::worker::worker(environment const & env, io_state const & ios, definition { lean_assert(todo_file); lock_guard lk(todo_file->m_lines_mutex); - todo_file->m_info.block_new_info(false); unsigned i = todo_file->find(todo_linenum); todo_file->m_snapshots.resize(i); s = i == 0 ? m_empty_snapshot : todo_file->m_snapshots[i-1]; lean_assert(s.m_line > 0); + todo_file->m_info.block_new_info(false); + todo_file->m_info.set_processed_upto(s.m_line); num_lines = todo_file->copy_to(block, s.m_line - 1); } if (m_terminate) @@ -244,6 +253,7 @@ static std::string g_clear_cache("CLEAR_CACHE"); static std::string g_echo("ECHO"); static std::string g_options("OPTIONS"); static std::string g_show("SHOW"); +static std::string g_valid("VALID"); static std::string g_sleep("SLEEP"); static bool is_command(std::string const & cmd, std::string const & line) { @@ -387,10 +397,10 @@ void server::show_options() { m_out << "-- ENDOPTIONS" << std::endl; } -void server::show() { +void server::show(bool valid) { check_file(); m_out << "-- BEGINSHOW" << std::endl; - m_file->show(m_out); + m_file->show(m_out, valid); m_out << "-- ENDSHOW" << std::endl; } @@ -435,7 +445,9 @@ bool server::operator()(std::istream & in) { } else if (is_command(g_wait, line)) { m_worker.wait(); } else if (is_command(g_show, line)) { - show(); + show(false); + } else if (is_command(g_valid, line)) { + show(true); } else if (is_command(g_sleep, line)) { unsigned ms = get_linenum(line, g_sleep); chrono::milliseconds d(ms); diff --git a/src/frontends/lean/server.h b/src/frontends/lean/server.h index 1d81fc691..2c587aefc 100644 --- a/src/frontends/lean/server.h +++ b/src/frontends/lean/server.h @@ -35,7 +35,7 @@ class server { void replace_line(unsigned linenum, std::string const & new_line); void insert_line(unsigned linenum, std::string const & new_line); void remove_line(unsigned linenum); - void show(std::ostream & out); + void show(std::ostream & out, bool valid); std::string const & get_fname() const { return m_fname; } info_manager const & infom() const { return m_info; } }; @@ -86,7 +86,7 @@ class server { void read_line(std::istream & in, std::string & line); void interrupt_worker(); void show_options(); - void show(); + void show(bool valid); unsigned get_linenum(std::string const & line, std::string const & cmd); public: