From 0cea63651deb91cf60129a7927ad83aca23a3985 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Feb 2015 10:38:37 -0800 Subject: [PATCH] fix(frontends/lean): store line/col information at snapshots, save snapshot before 'end' scope, and before "closing" open namespaces closes #422 --- src/frontends/lean/info_manager.cpp | 26 ++++++++++++++++---------- src/frontends/lean/info_manager.h | 2 +- src/frontends/lean/parser.cpp | 13 ++++++++----- src/frontends/lean/parser.h | 3 ++- src/frontends/lean/server.cpp | 2 +- 5 files changed, 28 insertions(+), 18 deletions(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index e8f6e5946..dca7f41df 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -303,13 +303,18 @@ struct info_manager::imp { */ struct env_info { unsigned m_line; + unsigned m_column; mutable unsigned m_iteration; environment m_env; options m_options; env_info():m_line(0), m_iteration(0) {} - env_info(unsigned l, unsigned i, environment const & env, options const & o): - m_line(l), m_iteration(i), m_env(env), m_options(o) {} - friend bool operator<(env_info const & i1, env_info const & i2) { return i1.m_line < i2.m_line; } + env_info(unsigned l, unsigned c, unsigned i, environment const & env, options const & o): + m_line(l), m_column(c), m_iteration(i), m_env(env), m_options(o) {} + friend bool operator<(env_info const & i1, env_info const & i2) { + if (i1.m_line != i2.m_line) + return i1.m_line < i2.m_line; + return i1.m_column < i2.m_column; + } }; mutex m_mutex; bool m_block_new_info; @@ -334,23 +339,24 @@ struct info_manager::imp { } } - void save_environment_options(unsigned l, environment const & env, options const & o) { + void save_environment_options(unsigned l, unsigned c, environment const & env, options const & o) { lock_guard lc(m_mutex); if (m_block_new_info) return; - // erase all entries in m_env_info such that e.m_line <= l and e.m_iteration < m_iteration + // erase all entries in m_env_info such that e.m_line <= l and e.m_column <= c and e.m_iteration < m_iteration auto it = m_env_info.begin(); auto end = m_env_info.end(); while (it != end) { - if (it->m_line > l) { + if (it->m_line > l || (it->m_line == l && it->m_column > c)) { break; - } else if (it->m_line <= l && it->m_iteration < m_iteration) { + } else if ((it->m_line < l || (it->m_line == l && it->m_column <= c)) && + it->m_iteration < m_iteration) { m_env_info.erase(it++); } else { ++it; } } - env_info info(l, m_iteration, env, o); + env_info info(l, c, m_iteration, env, o); m_env_info.erase(info); m_env_info.insert(info); } @@ -746,8 +752,8 @@ void info_manager::invalidate_line_col(unsigned l, unsigned c) { m_ptr->invalida 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); +void info_manager::save_environment_options(unsigned l, unsigned c, environment const & env, options const & o) { + m_ptr->save_environment_options(l, c, env, o); } void info_manager::clear() { m_ptr->clear(); } optional> info_manager::get_final_env_opts() const { return m_ptr->get_final_env_opts(); } diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index fb50db2bb..19299f727 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -43,7 +43,7 @@ public: 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); + void save_environment_options(unsigned l, unsigned col, environment const & env, options const & o); optional> get_final_env_opts() const; optional> get_closest_env_opts(unsigned linenum) const; optional get_type_at(unsigned line, unsigned col) const; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 09e983770..f1d41fddb 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1415,13 +1415,13 @@ void parser::parse_imports() { }); } if (imported) - commit_info(1); + commit_info(1, 0); } -void parser::commit_info(unsigned line) { +void parser::commit_info(unsigned line, unsigned col) { save_snapshot(); if (m_info_manager) { - m_info_manager->save_environment_options(line, m_env, m_ios.get_options()); + m_info_manager->save_environment_options(line, col, m_env, m_ios.get_options()); m_info_manager->commit_upto(line, true); } } @@ -1451,8 +1451,10 @@ bool parser::parse_commands() { check_interrupted(); switch (curr()) { case scanner::token_kind::CommandKeyword: + if (curr_is_token(get_end_tk())) + commit_info(); parse_command(); - commit_info(m_scanner.get_line()); + commit_info(); break; case scanner::token_kind::ScriptBlock: parse_script(); @@ -1480,10 +1482,11 @@ bool parser::parse_commands() { throw_parser_exception("invalid end of module, expecting 'end'", pos()); } } catch (interrupt_parser) { + commit_info(); while (has_open_scopes(m_env)) m_env = pop_scope_core(m_env); } - commit_info(m_scanner.get_line()+1); + commit_info(m_scanner.get_line()+1, 0); for (certified_declaration const & thm : m_theorem_queue.join()) { if (keep_new_thms()) m_env.replace(thm); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index b090199a0..b5f57553d 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -212,7 +212,8 @@ class parser { void save_type_info(expr const & e); void save_pre_info_data(); void save_identifier_info(pos_info const & p, name const & full_id); - void commit_info(unsigned line); + void commit_info(unsigned line, unsigned col); + void commit_info() { commit_info(m_scanner.get_line(), m_scanner.get_pos()); } elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true); elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp); diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index de88a94b0..4c6a2bfb3 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -193,7 +193,7 @@ server::worker::worker(environment const & env, io_state const & ios, definition s = m_empty_snapshot; lean_assert(s.m_line > 0); todo_file->m_info.start_from(s.m_line); - todo_file->m_info.save_environment_options(s.m_line, s.m_env, s.m_options); + todo_file->m_info.save_environment_options(s.m_line, 0, s.m_env, s.m_options); num_lines = todo_file->copy_to(block, s.m_line - 1); } if (m_terminate)