diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index c484112b1..9366ea372 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -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) {
diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h
index 8fc31c058..d5720db47 100644
--- a/src/frontends/lean/info_manager.h
+++ b/src/frontends/lean/info_manager.h
@@ -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);
diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index 88dca0db2..cce370667 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -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;
 }