michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean): store line/col information at snapshots, save snapshot before 'end' scope, and before "closing" open namespaces

Browse source 
closes #422
This commit is contained in:
Leonardo de Moura 2015-02-04 10:38:37 -08:00
parent 420da8fd3f
commit 0cea63651d
5 changed files with 28 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/frontends/lean/info_manager.cpp
View file

@ -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<mutex> 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<pair<environment, options>> info_manager::get_final_env_opts() const { return m_ptr->get_final_env_opts(); }

2
src/frontends/lean/info_manager.h
View file

@ -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<pair<environment, options>> get_final_env_opts() const;
optional<pair<environment, options>> get_closest_env_opts(unsigned linenum) const;
optional<expr> get_type_at(unsigned line, unsigned col) const;

13
src/frontends/lean/parser.cpp
View file

@ -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);

3
src/frontends/lean/parser.h
View file

@ -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);

2
src/frontends/lean/server.cpp
View file

@ -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)