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

feat(frontends/lean/server): preserve info that occurs in columns before first changed column

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-27 21:09:52 -07:00
parent 00a049a667
commit 1a8eb9799e
3 changed files with 27 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -365,15 +365,32 @@ struct info_manager::imp {
m_processed_upto = l - 1;
}
void invalidate_line(unsigned l) {
void invalidate_line_col_core(unsigned l, optional<unsigned> const & c) {
lock_guard<mutex> lc(m_mutex);
synch_line(l);
if (m_processed_upto > l - 1)
m_processed_upto = l - 1;
m_line_data[l] = info_data_set();
if (!c) {
m_line_data[l] = info_data_set();
} else {
info_data_set new_set;
m_line_data[l].for_each([&](info_data const & d) {
if (d.get_column() < *c)
new_set.insert(d);
});
m_line_data[l] = new_set;
}
m_line_valid[l] = false;
}
void invalidate_line(unsigned l) {
invalidate_line_col_core(l, optional<unsigned>());
}
void invalidate_line_col(unsigned l, unsigned c) {
invalidate_line_col_core(l, optional<unsigned>(c));
}
void commit_upto(unsigned l, bool valid) {
lock_guard<mutex> lc(m_mutex);
if (m_block_new_info)
@ -462,6 +479,7 @@ void info_manager::merge(info_manager const & m, bool overwrite) { m_ptr->merge(
void info_manager::insert_line(unsigned l) { m_ptr->insert_line(l); }
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); }
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) {

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

@ -29,6 +29,7 @@ public:
void insert_line(unsigned l);
void remove_line(unsigned l);
void invalidate_line(unsigned l);
void invalidate_line_col(unsigned l, unsigned c);
void commit_upto(unsigned l, bool valid);
bool is_invalidated(unsigned l) const;
void save_environment_options(unsigned l, environment const & env, options const & o);

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

@ -19,10 +19,14 @@ server::file::file(std::istream & in, std::string const & fname):m_fname(fname)
void server::file::replace_line(unsigned linenum, std::string const & new_line) {
lock_guard<mutex> lk(m_lines_mutex);
m_info.block_new_info(true);
m_info.invalidate_line(linenum+1);
while (linenum >= m_lines.size())
m_lines.push_back("");
std::string const & old_line = m_lines[linenum];
unsigned i = 0;
while (i < old_line.size() && i < new_line.size() && old_line[i] == new_line[i])
i++;
m_info.block_new_info(true);
m_info.invalidate_line_col(linenum+1, i);
m_lines[linenum] = new_line;
}