diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 3d90c1334..5bdee3306 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -187,6 +187,7 @@ struct decl_modifiers {
 
 environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     auto n_pos = p.pos();
+    unsigned start_line = n_pos.first;
     name n     = p.check_id_next("invalid declaration, identifier expected");
     check_atomic(n);
     decl_modifiers modifiers;
@@ -246,6 +247,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
     }
+    unsigned end_line = p.pos().first;
 
     if (p.used_sorry())
         p.declare_sorry();
@@ -277,23 +279,26 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     expr pre_value = value;
     level_param_names new_ls;
     bool found_cached = false;
-    if (auto it = p.find_cached_definition(real_n, pre_type, pre_value)) {
-        optional<certified_declaration> cd;
-        try {
-            level_param_names c_ls; expr c_type, c_value;
-            std::tie(c_ls, c_type, c_value) = *it;
-            if (is_theorem)
-                cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value));
-            else
-                cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, modifiers.m_is_opaque));
-            env = module::add(env, *cd);
-            found_cached = true;
-        } catch (exception&) {}
+    if (p.are_info_lines_valid(start_line, end_line)) {
+        // we only use the cache if the information associated with the line is valid
+        if (auto it = p.find_cached_definition(real_n, pre_type, pre_value)) {
+            optional<certified_declaration> cd;
+            try {
+                level_param_names c_ls; expr c_type, c_value;
+                std::tie(c_ls, c_type, c_value) = *it;
+                if (is_theorem)
+                    cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value));
+                else
+                    cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, modifiers.m_is_opaque));
+                env = module::add(env, *cd);
+                found_cached = true;
+            } catch (exception&) {}
+        }
     }
 
     if (!found_cached) {
         if (is_theorem) {
-            if (p.num_threads() > 1) {
+            if (!p.collecting_info() && p.num_threads() > 1) {
                 // add as axiom, and create a task to prove the theorem
                 p.add_delayed_theorem(env, real_n, ls, type, value);
                 std::tie(type, new_ls) = p.elaborate_type(type);
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2ce5f289e..18d8b6337 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -307,7 +307,7 @@ class elaborator {
     name_set             m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
     bool                 m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent.
     bool                 m_noinfo;  // when true, we do not collect information when true, we set is to true whenever we find noinfo annotation.
-    std::vector<info_data> m_pre_info_data;
+    info_manager         m_pre_info_data;
 
     struct scope_ctx {
         context::scope m_scope1;
@@ -858,7 +858,7 @@ public:
             }
             if (!first) {
                 // we save the info data again for application of functions with strict implicit arguments
-                replace_info_data(get_app_fn(e), f);
+                save_info_data(get_app_fn(e), f);
             }
         }
         expr d_type = binding_domain(f_type);
@@ -904,33 +904,20 @@ public:
     }
 
     /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
-    void save_info_data_core(expr const & e, expr const & r, bool replace) {
+    void save_info_data(expr const & e, expr const & r) {
         if (!m_noinfo && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
             if (auto p = pip()->get_pos_info(e)) {
                 type_checker::scope scope(*m_tc[m_relax_main_opaque]);
                 expr t = m_tc[m_relax_main_opaque]->infer(r);
-                info_data d = mk_type_info(p->first, p->second, t);
-                if (replace) {
-                    while (!m_pre_info_data.empty() && m_pre_info_data.back() == d)
-                        m_pre_info_data.pop_back();
-                }
-                m_pre_info_data.push_back(d);
+                m_pre_info_data.add_type_info(p->first, p->second, t);
             }
         }
     }
 
-    void save_info_data(expr const & e, expr const & r) {
-        save_info_data_core(e, r, false);
-    }
-
-    void replace_info_data(expr const & e, expr const & r) {
-        save_info_data_core(e, r, true);
-    }
-
     void save_synth_data(expr const & e, expr const & r) {
         if (!m_noinfo && infom() && pip() && is_placeholder(e)) {
             if (auto p = pip()->get_pos_info(e)) {
-                m_pre_info_data.push_back(mk_synth_info(p->first, p->second, r));
+                m_pre_info_data.add_synth_info(p->first, p->second, r);
             }
         }
     }
@@ -1271,10 +1258,8 @@ public:
     void copy_info_to_manager(substitution s) {
         if (!infom())
             return;
-        for (auto & p : m_pre_info_data)
-            p = p.instantiate(s);
-        // TODO(Leo): implement smarter append
-        infom()->append(m_pre_info_data, false);
+        m_pre_info_data.instantiate(s);
+        infom()->merge(m_pre_info_data);
         m_pre_info_data.clear();
     }
 
diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index e80b1be3a..d72473a3c 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -4,34 +4,65 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <algorithm>
 #include <vector>
+#include "util/thread.h"
 #include "library/choice.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/pp_options.h"
 
 namespace lean {
-void info_data_cell::dealloc() { delete this; }
+class info_data;
 
-int info_data_cell::compare(info_data_cell const & d) const {
-    if (m_line != d.m_line)
-        return m_line < d.m_line ? -1 : 1;
-    if (m_column != d.m_column)
-        return m_column < d.m_column ? -1 : 1;
-    if (typeid(*this) != typeid(d))
-        return typeid(*this).before(typeid(d)) ? -1 : 1;
-    return 0;
-}
-
-info_data_cell * info_data_cell::instantiate(substitution &) const { return nullptr; }
-
-struct tmp_info_data : public info_data_cell {
-    tmp_info_data(unsigned l, unsigned c):info_data_cell(l, c) {}
-    virtual void display(io_state_stream const &) const { lean_unreachable(); } // LCOV_EXCL_LINE
+class info_data_cell {
+    unsigned m_column;
+    MK_LEAN_RC();
+    void dealloc() { delete this; }
+protected:
+    friend info_data;
+    virtual info_data_cell * instantiate(substitution &) const { return nullptr; }
+public:
+    info_data_cell():m_column(0), m_rc(0) {}
+    info_data_cell(unsigned c):m_column(c), m_rc(0) {}
+    virtual ~info_data_cell() {}
+    unsigned get_column() const { return m_column; }
+    virtual void display(io_state_stream const & ios, unsigned line) const = 0;
+    virtual int compare(info_data_cell const & d) const {
+        if (m_column != d.m_column)
+            return m_column < d.m_column ? -1 : 1;
+        if (typeid(*this) != typeid(d))
+            return typeid(*this).before(typeid(d)) ? -1 : 1;
+        return 0;
+    }
 };
 
-static info_data g_dummy(new tmp_info_data(0, 0));
+class info_data {
+private:
+    info_data_cell * m_ptr;
+public:
+    info_data();
+    info_data(info_data_cell * c):m_ptr(c) { lean_assert(c); m_ptr->inc_ref(); }
+    info_data(info_data const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    info_data(info_data && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    ~info_data() { if (m_ptr) m_ptr->dec_ref(); }
+    friend void swap(info_data & a, info_data & b) { std::swap(a.m_ptr, b.m_ptr); }
+    info_data & operator=(info_data const & s) { LEAN_COPY_REF(s); }
+    info_data & operator=(info_data && s) { LEAN_MOVE_REF(s); }
+    int compare(info_data const & d) const { return m_ptr->compare(*d.m_ptr); }
+    int compare(info_data_cell const & d) const { return m_ptr->compare(d); }
+    info_data instantiate(substitution & s) const;
+    unsigned get_column() const { return m_ptr->get_column(); }
+    void display(io_state_stream const & ios, unsigned line) const { m_ptr->display(ios, line); }
+};
 
+struct tmp_info_data : public info_data_cell {
+    tmp_info_data(unsigned c):info_data_cell(c) {}
+    virtual void display(io_state_stream const &, unsigned) const { lean_unreachable(); } // LCOV_EXCL_LINE
+};
+
+static info_data g_dummy(new tmp_info_data(0));
 info_data::info_data():info_data(g_dummy) {}
+
 info_data info_data::instantiate(substitution & s) const {
     if (auto r = m_ptr->instantiate(s)) {
         return info_data(r);
@@ -45,14 +76,14 @@ protected:
     expr m_expr;
 public:
     type_info_data() {}
-    type_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_expr(e) {}
+    type_info_data(unsigned c, expr const & e):info_data_cell(c), m_expr(e) {}
 
     expr const & get_type() const {
         return m_expr;
     }
 
-    virtual void display(io_state_stream const & ios) const {
-        ios << "-- TYPE|" << get_line() << "|" << get_column() << "\n";
+    virtual void display(io_state_stream const & ios, unsigned line) const {
+        ios << "-- TYPE|" << line << "|" << get_column() << "\n";
         ios << m_expr << endl;
         ios << "-- ACK" << endl;
     }
@@ -62,15 +93,15 @@ public:
         if (is_eqp(e, m_expr))
             return nullptr;
         else
-            return new type_info_data(get_line(), get_column(), e);
+            return new type_info_data(get_column(), e);
     }
 };
 
 class synth_info_data : public type_info_data {
 public:
-    synth_info_data(unsigned l, unsigned c, expr const & e):type_info_data(l, c, e) {}
-    virtual void display(io_state_stream const & ios) const {
-        ios << "-- SYNTH|" << get_line() << "|" << get_column() << "\n";
+    synth_info_data(unsigned c, expr const & e):type_info_data(c, e) {}
+    virtual void display(io_state_stream const & ios, unsigned line) const {
+        ios << "-- SYNTH|" << line << "|" << get_column() << "\n";
         ios << m_expr << endl;
         ios << "-- ACK" << endl;
     }
@@ -79,9 +110,9 @@ public:
 class overload_info_data : public info_data_cell {
     expr m_choices;
 public:
-    overload_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_choices(e) {}
-    virtual void display(io_state_stream const & ios) const {
-        ios << "-- OVERLOAD|" << get_line() << "|" << get_column() << "\n";
+    overload_info_data(unsigned c, expr const & e):info_data_cell(c), m_choices(e) {}
+    virtual void display(io_state_stream const & ios, unsigned line) const {
+        ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n";
         options os = ios.get_options();
         os = os.update(get_pp_full_names_option_name(), true);
         auto new_ios = ios.update_options(os);
@@ -97,9 +128,9 @@ public:
 class coercion_info_data : public info_data_cell {
     expr m_coercion;
 public:
-    coercion_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_coercion(e) {}
-    virtual void display(io_state_stream const & ios) const {
-        ios << "-- COERCION|" << get_line() << "|" << get_column() << "\n";
+    coercion_info_data(unsigned c, expr const & e):info_data_cell(c), m_coercion(e) {}
+    virtual void display(io_state_stream const & ios, unsigned line) const {
+        ios << "-- COERCION|" << line << "|" << get_column() << "\n";
         options os = ios.get_options();
         os = os.update(get_pp_coercion_option_name(), true);
         ios.update_options(os) << m_coercion << endl;
@@ -107,105 +138,174 @@ public:
     }
 };
 
-info_data mk_type_info(unsigned l, unsigned c, expr const & e) { return info_data(new type_info_data(l, c, e)); }
-info_data mk_synth_info(unsigned l, unsigned c, expr const & e) { return info_data(new synth_info_data(l, c, e)); }
-info_data mk_overload_info(unsigned l, unsigned c, expr const & e) { return info_data(new overload_info_data(l, c, e)); }
-info_data mk_coercion_info(unsigned l, unsigned c, expr const & e) { return info_data(new coercion_info_data(l, c, e)); }
+info_data mk_type_info(unsigned c, expr const & e) { return info_data(new type_info_data(c, e)); }
+info_data mk_synth_info(unsigned c, expr const & e) { return info_data(new synth_info_data(c, e)); }
+info_data mk_overload_info(unsigned c, expr const & e) { return info_data(new overload_info_data(c, e)); }
+info_data mk_coercion_info(unsigned c, expr const & e) { return info_data(new coercion_info_data(c, e)); }
 
-bool operator<(info_data const & i1, info_data const & i2) { return i1.compare(i2) < 0; }
-bool operator==(info_data const & i1, info_data const & i2) { return i1.compare(i2) == 0; }
-bool operator!=(info_data const & i1, info_data const & i2) { return i1.compare(i2) != 0; }
-bool operator<(info_data const & i1, info_data_cell const & i2) { return i1.compare(i2) < 0; }
+struct info_data_cmp {
+    int operator()(info_data const & i1, info_data const & i2) const { return i1.compare(i2); }
+};
 
-info_manager::info_manager():m_sorted_upto(0) {}
+struct info_manager::imp {
+    typedef rb_tree<info_data, info_data_cmp> info_data_set;
+    mutex                      m_mutex;
+    std::vector<info_data_set> m_line_data;
+    std::vector<bool>          m_line_valid;
+    unsigned                   m_available_upto;
 
-void info_manager::sort_core() {
-    if (m_sorted_upto == m_data.size())
-        return;
-    std::stable_sort(m_data.begin() + m_sorted_upto, m_data.end());
-    m_sorted_upto = m_data.size();
-}
+    imp():m_available_upto(0) {}
 
-/**
-   \brief Return index i <= m_sorted_upto s.t.
-      * forall j < i, m_data[j].pos < (line, column)
-      * forall i <= j < m_sorted_upto,  m_data[j].pos >= (line, column)
-*/
-unsigned info_manager::find(unsigned line, unsigned column) {
-    tmp_info_data d(line, column);
-    unsigned low  = 0;
-    unsigned high = m_sorted_upto;
-    while (true) {
-        // forall j < low,                    m_data[j] < d
-        // forall high <= j < m_sorted_upto,  m_data[j] >= d
-        lean_assert(low <= high);
-        if (low == high)
-            return low;
-        unsigned mid = low + ((high - low)/2);
-        lean_assert(low <= mid && mid < high);
-        lean_assert(mid < m_sorted_upto);
-        info_data const & dmid = m_data[mid];
-        if (dmid < d) {
-            low  = mid+1;
-        } else {
-            high = mid;
+    void synch_line(unsigned l) {
+        lean_assert(l > 0);
+        if (l >= m_line_data.size()) {
+            m_line_data.resize(l+1);
+            m_line_valid.resize(l+1, true);
         }
     }
-}
 
-void info_manager::invalidate(unsigned sline) {
-    lock_guard<mutex> lc(m_mutex);
-    sort_core();
-    unsigned i = find(sline, 0);
-    m_data.resize(i);
-    if (m_data.size() < m_sorted_upto)
-        m_sorted_upto = m_data.size();
-}
-
-void info_manager::add_core(info_data const & d) {
-    if (m_data.empty()) {
-        m_sorted_upto = 1;
-    } else if (m_sorted_upto == m_data.size() && m_data.back() < d) {
-        m_sorted_upto++;
-    } else if (m_sorted_upto > 0 && d < m_data[m_sorted_upto-1]) {
-        m_sorted_upto = find(d.get_line(), d.get_column());
+    void add_type_info(unsigned l, unsigned c, expr const & e) {
+        lock_guard<mutex> lc(m_mutex);
+        synch_line(l);
+        m_line_data[l].insert(mk_type_info(c, e));
     }
-    m_data.push_back(d);
-}
 
-void info_manager::add(info_data const & d) {
-    lock_guard<mutex> lc(m_mutex);
-    add_core(d);
-}
+    void add_synth_info(unsigned l, unsigned c, expr const & e) {
+        lock_guard<mutex> lc(m_mutex);
+        synch_line(l);
+        m_line_data[l].insert(mk_synth_info(c, e));
+    }
 
-void info_manager::append(std::vector<info_data> & vs, bool remove_duplicates) {
-    lock_guard<mutex> lc(m_mutex);
-    std::stable_sort(vs.begin(), vs.end());
-    info_data prev;
-    bool first = true;
-    for (auto const & v : vs) {
-        if (!remove_duplicates || first || v != prev) {
-            prev = v;
-            add_core(v);
-            first = false;
+    void add_overload_info(unsigned l, unsigned c, expr const & e) {
+        lock_guard<mutex> lc(m_mutex);
+        synch_line(l);
+        m_line_data[l].insert(mk_overload_info(c, e));
+    }
+
+    void add_coercion_info(unsigned l, unsigned c, expr const & e) {
+        lock_guard<mutex> lc(m_mutex);
+        synch_line(l);
+        m_line_data[l].insert(mk_coercion_info(c, e));
+    }
+
+    static info_data_set instantiate(info_data_set const & s, substitution & subst) {
+        info_data_set r;
+        s.for_each([&](info_data const & d) {
+                r.insert(d.instantiate(subst));
+            });
+        return r;
+    }
+
+    void instantiate(substitution const & s) {
+        lock_guard<mutex> lc(m_mutex);
+        substitution tmp_s = s;
+        unsigned sz     = m_line_data.size();
+        for (unsigned i = 0; i < sz; i++) {
+            m_line_data[i] = instantiate(m_line_data[i], tmp_s);
         }
     }
-}
 
-void info_manager::sort() {
-    lock_guard<mutex> lc(m_mutex);
-    sort_core();
-}
-
-void info_manager::display(io_state_stream const & ios, unsigned line) {
-    lock_guard<mutex> lc(m_mutex);
-    sort_core();
-    unsigned i = find(line, 0);
-    for (; i < m_data.size(); i++) {
-        auto const & d = m_data[i];
-        if (d.get_line() > line)
-            break;
-        d.display(ios);
+    void merge(info_manager::imp const & m) {
+        if (m.m_line_data.empty())
+            return;
+        lock_guard<mutex> lc(m_mutex);
+        unsigned sz = m.m_line_data.size();
+        for (unsigned i = 1; i < sz; i++) {
+            info_data_set const & s = m.m_line_data[i];
+            s.for_each([&](info_data const & d) {
+                    synch_line(i);
+                    m_line_data[i].insert(d);
+                });
+        }
     }
-}
+
+    void insert_line(unsigned l) {
+        lock_guard<mutex> lc(m_mutex);
+        synch_line(l);
+        if (m_available_upto > l - 1)
+            m_available_upto = l - 1;
+        m_line_data.push_back(info_data_set());
+        unsigned i = m_line_data.size();
+        while (i > l) {
+            --i;
+            m_line_data[i]  = m_line_data[i-1];
+            m_line_valid[i] = m_line_valid[i-1];
+        }
+        m_line_valid[l] = false;
+    }
+
+    void remove_line(unsigned l) {
+        lock_guard<mutex> lc(m_mutex);
+        lean_assert(l > 0);
+        if (l >= m_line_data.size())
+            return;
+        lean_assert(!m_line_data.empty());
+        for (unsigned i = l; i < m_line_data.size() - 1; i++) {
+            m_line_data[i]  = m_line_data[i+1];
+            m_line_valid[i] = m_line_valid[i+1];
+        }
+        m_line_data.pop_back();
+        if (m_available_upto > l - 1)
+            m_available_upto = l - 1;
+    }
+
+    void invalidate_line(unsigned l) {
+        lock_guard<mutex> lc(m_mutex);
+        synch_line(l);
+        if (m_available_upto > l - 1)
+            m_available_upto = l - 1;
+        m_line_data[l]  = info_data_set();
+        m_line_valid[l] = false;
+    }
+
+    void commit_upto(unsigned l, bool valid) {
+        lock_guard<mutex> lc(m_mutex);
+        for (unsigned i = m_available_upto; i < l && i < m_line_valid.size(); i++)
+            m_line_valid[i] = valid;
+        m_available_upto = l;
+    }
+
+    bool is_available(unsigned l) {
+        lock_guard<mutex> lc(m_mutex);
+        return l < m_available_upto;
+    }
+
+    bool is_invalidated(unsigned l) {
+        lock_guard<mutex> lc(m_mutex);
+        if (l >= m_line_valid.size())
+            return false;
+        return !m_line_valid[l];
+    }
+
+    void display(io_state_stream const & ios, unsigned l) {
+        lock_guard<mutex> lc(m_mutex);
+        if (l >= m_line_data.size())
+            return;
+        m_line_data[l].for_each([&](info_data const & d) {
+                d.display(ios, l);
+            });
+    }
+
+    void clear() {
+        lock_guard<mutex> lc(m_mutex);
+        m_line_data.clear();
+    }
+};
+
+info_manager::info_manager():m_ptr(new imp()) {}
+info_manager::~info_manager() {}
+void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_type_info(l, c, e); }
+void info_manager::add_synth_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_synth_info(l, c, e); }
+void info_manager::add_overload_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_overload_info(l, c, e); }
+void info_manager::add_coercion_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_coercion_info(l, c, e); }
+void info_manager::instantiate(substitution const & s) { m_ptr->instantiate(s); }
+void info_manager::merge(info_manager const & m) { m_ptr->merge(*m.m_ptr); }
+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::commit_upto(unsigned l, bool valid) { m_ptr->commit_upto(l, valid); }
+bool info_manager::is_available(unsigned l) const { return m_ptr->is_available(l); }
+bool info_manager::is_invalidated(unsigned l) const { return m_ptr->is_invalidated(l); }
+void info_manager::clear() { m_ptr->clear(); }
+void info_manager::display(io_state_stream const & ios, unsigned line) { m_ptr->display(ios, line); }
 }
diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h
index 2faf48f61..65f498e33 100644
--- a/src/frontends/lean/info_manager.h
+++ b/src/frontends/lean/info_manager.h
@@ -6,72 +6,31 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <vector>
-#include "util/thread.h"
 #include "kernel/expr.h"
 #include "kernel/metavar.h"
 #include "library/io_state_stream.h"
 
 namespace lean {
-class info_data;
-class info_data_cell {
-    unsigned m_line;
-    unsigned m_column;
-    MK_LEAN_RC();
-    void dealloc();
-protected:
-    friend info_data;
-    virtual info_data_cell * instantiate(substitution &) const;
-public:
-    info_data_cell():m_line(0), m_column(0), m_rc(0) {}
-    info_data_cell(unsigned l, unsigned c):m_line(l), m_column(c) {}
-    virtual ~info_data_cell() {}
-    unsigned get_line() const { return m_line; }
-    unsigned get_column() const { return m_column; }
-    virtual int compare(info_data_cell const & d) const;
-    virtual void display(io_state_stream const & ios) const = 0;
-};
-
-class info_data {
-private:
-    info_data_cell * m_ptr;
-public:
-    info_data();
-    info_data(info_data_cell * c):m_ptr(c) { lean_assert(c); m_ptr->inc_ref(); }
-    info_data(info_data const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    info_data(info_data && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-    ~info_data() { if (m_ptr) m_ptr->dec_ref(); }
-    friend void swap(info_data & a, info_data & b) { std::swap(a.m_ptr, b.m_ptr); }
-    info_data & operator=(info_data const & s) { LEAN_COPY_REF(s); }
-    info_data & operator=(info_data && s) { LEAN_MOVE_REF(s); }
-    void display(io_state_stream const & ios) const { m_ptr->display(ios); }
-    int compare(info_data const & d) const { return m_ptr->compare(*d.m_ptr); }
-    int compare(info_data_cell const & d) const { return m_ptr->compare(d); }
-    info_data instantiate(substitution & s) const;
-    unsigned get_line() const { return m_ptr->get_line(); }
-    unsigned get_column() const { return m_ptr->get_column(); }
-};
-bool operator==(info_data const & i1, info_data const & i2);
-
-info_data mk_type_info(unsigned l, unsigned c, expr const & e);
-info_data mk_synth_info(unsigned l, unsigned c, expr const & e);
-info_data mk_overload_info(unsigned l, unsigned c, expr const & e);
-info_data mk_coercion_info(unsigned l, unsigned c, expr const & e);
-
 class info_manager {
-    typedef std::vector<info_data> data_vector;
-    mutex       m_mutex;
-
-    unsigned    m_sorted_upto;
-    data_vector m_data;
-    void add_core(info_data const & d);
-    unsigned find(unsigned line, unsigned column);
-    void sort_core();
+    struct imp;
+    std::unique_ptr<imp> m_ptr;
 public:
     info_manager();
-    void invalidate(unsigned sline);
-    void add(info_data const & d);
-    void append(std::vector<info_data> & v, bool remove_duplicates = true);
-    void sort();
+    ~info_manager();
+
+    void add_type_info(unsigned l, unsigned c, expr const & e);
+    void add_synth_info(unsigned l, unsigned c, expr const & e);
+    void add_overload_info(unsigned l, unsigned c, expr const & e);
+    void add_coercion_info(unsigned l, unsigned c, expr const & e);
+    void instantiate(substitution const & s);
+    void merge(info_manager const & m);
+    void insert_line(unsigned l);
+    void remove_line(unsigned l);
+    void invalidate_line(unsigned l);
+    void commit_upto(unsigned l, bool valid);
+    bool is_available(unsigned l) const;
+    bool is_invalidated(unsigned l) const;
+    void clear();
     void display(io_state_stream const & ios, unsigned line);
 };
 }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index fc569b129..47fe9f5a7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -131,6 +131,15 @@ void parser::add_ref_index(name const & n, pos_info const & pos) {
         m_index->add_ref(get_stream_name(), pos, n);
 }
 
+bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const {
+    if (!m_info_manager)
+        return true; // we are not tracking info
+    for (unsigned i = start_line; i <= end_line; i++)
+        if (m_info_manager->is_invalidated(i))
+            return false;
+    return true;
+}
+
 expr parser::mk_sorry(pos_info const & p) {
     m_used_sorry = true;
     {
@@ -235,6 +244,8 @@ void parser::sync_command() {
     // Keep consuming tokens until we find a Command or End-of-file
     while (curr() != scanner::token_kind::CommandKeyword && curr() != scanner::token_kind::Eof)
         next();
+    if (m_info_manager)
+        m_info_manager->commit_upto(m_scanner.get_line()+1, false);
 }
 
 tag parser::get_tag(expr e) {
@@ -546,7 +557,7 @@ std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, li
     parser_pos_provider pp = get_pos_provider();
     elaborator_context env = mk_elaborator_context(pp, check_unassigned);
     auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
-    m_pre_info_data.clear();
+    m_pre_info_manager.clear();
     return r;
 }
 
@@ -557,7 +568,7 @@ std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<
     parser_pos_provider pp = get_pos_provider();
     elaborator_context env = mk_elaborator_context(pp, check_unassigned);
     auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
-    m_pre_info_data.clear();
+    m_pre_info_manager.clear();
     return r;
 }
 
@@ -566,7 +577,7 @@ std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env
     parser_pos_provider pp = get_pos_provider();
     elaborator_context eenv = mk_elaborator_context(env, pp);
     auto r = ::lean::elaborate(eenv, list<expr>(), e, relax);
-    m_pre_info_data.clear();
+    m_pre_info_manager.clear();
     return r;
 }
 
@@ -575,7 +586,7 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
     parser_pos_provider pp = get_pos_provider();
     elaborator_context eenv = mk_elaborator_context(pp);
     auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
-    m_pre_info_data.clear();
+    m_pre_info_manager.clear();
     return r;
 }
 
@@ -584,7 +595,7 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(enviro
     parser_pos_provider pp = get_pos_provider();
     elaborator_context eenv = mk_elaborator_context(env, lls, pp);
     auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
-    m_pre_info_data.clear();
+    m_pre_info_manager.clear();
     return r;
 }
 
@@ -1210,6 +1221,8 @@ bool parser::parse_commands() {
                     case scanner::token_kind::CommandKeyword:
                         parse_command();
                         save_snapshot();
+                        if (m_info_manager)
+                            m_info_manager->commit_upto(m_scanner.get_line(), true);
                         break;
                     case scanner::token_kind::ScriptBlock:
                         parse_script();
@@ -1238,6 +1251,8 @@ bool parser::parse_commands() {
         }
     } catch (interrupt_parser) {}
     save_snapshot();
+    if (m_info_manager)
+        m_info_manager->commit_upto(m_scanner.get_line()+1, true);
     for (certified_declaration const & thm : m_theorem_queue.join()) {
         m_env.replace(thm);
     }
@@ -1249,7 +1264,7 @@ void parser::add_delayed_theorem(environment const & env, name const & n, level_
 }
 
 void parser::save_snapshot() {
-    m_pre_info_data.clear();
+    m_pre_info_manager.clear();
     if (!m_snapshot_vector)
         return;
     if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
@@ -1259,8 +1274,8 @@ void parser::save_snapshot() {
 void parser::save_pre_info_data() {
     // if elaborator failed, then m_pre_info_data contains type information before elaboration.
     if (m_info_manager) {
-        m_info_manager->append(m_pre_info_data, false);
-        m_pre_info_data.clear();
+        m_info_manager->merge(m_pre_info_manager);
+        m_pre_info_manager.clear();
     }
 }
 
@@ -1268,7 +1283,7 @@ void parser::save_overload(expr const & e) {
     if (!m_info_manager || !is_choice(e))
         return;
     auto p = pos_of(e);
-    m_info_manager->add(mk_overload_info(p.first, p.second, e));
+    m_info_manager->add_overload_info(p.first, p.second, e);
 }
 
 void parser::save_type_info(expr const & e) {
@@ -1288,13 +1303,13 @@ void parser::save_type_info(expr const & e) {
         if (!d)
             return;
         auto p = pos_of(e);
-        m_pre_info_data.push_back(mk_type_info(p.first, p.second, d->get_type()));
+        m_pre_info_manager.add_type_info(p.first, p.second, d->get_type());
     } else if (is_local(e)) {
         auto p = pos_of(e);
         expr t = mlocal_type(e);
         if (is_meta(t))
             return;
-        m_pre_info_data.push_back(mk_type_info(p.first, p.second, t));
+        m_pre_info_manager.add_type_info(p.first, p.second, t);
     }
 }
 
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 2a8993806..9ac0aa869 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -91,7 +91,7 @@ class parser {
     // info support
     snapshot_vector *       m_snapshot_vector;
     info_manager *          m_info_manager;
-    std::vector<info_data>  m_pre_info_data; // type information before elaboration
+    info_manager            m_pre_info_manager; // type information before elaboration
 
     // cache support
     definition_cache *     m_cache;
@@ -186,6 +186,9 @@ public:
     optional<std::tuple<level_param_names, expr, expr>> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value);
     void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); }
 
+    bool are_info_lines_valid(unsigned start_line, unsigned end_line) const;
+    bool collecting_info() const { return m_info_manager; }
+
     void set_index(declaration_index * i) { m_index = i; }
     void add_decl_index(name const & n, pos_info const & pos);
     void add_ref_index(name const & n, pos_info const & pos);
diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index 29672b545..a7c495035 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -68,7 +68,6 @@ unsigned server::file::find(unsigned linenum) {
 server::server(environment const & env, io_state const & ios, unsigned num_threads):
     m_env(env), m_ios(ios), m_out(ios.get_regular_channel().get_stream()),
     m_num_threads(num_threads), m_empty_snapshot(m_env, m_ios.get_options()) {
-    m_thread_busy = false;
 }
 
 server::~server() {
@@ -86,7 +85,6 @@ void server::reset_thread() {
         m_thread_ptr->join();
         m_thread_ptr.reset(nullptr);
     }
-    m_thread_busy = false;
 }
 
 static std::string g_load("LOAD");
@@ -98,6 +96,7 @@ static std::string g_check("CHECK");
 static std::string g_info("INFO");
 static std::string g_set("SET");
 static std::string g_eval("EVAL");
+static std::string g_wait("WAIT");
 
 static bool is_command(std::string const & cmd, std::string const & line) {
     return line.compare(0, cmd.size(), cmd) == 0;
@@ -137,13 +136,10 @@ void server::process_from(unsigned linenum) {
     snapshot & s = i == 0 ? m_empty_snapshot : m_file->m_snapshots[i-1];
     std::string block;
     lean_assert(s.m_line > 0);
-    m_file->m_info.invalidate(s.m_line-1);
     for (unsigned j = s.m_line-1; j < m_file->m_lines.size(); j++) {
         block += m_file->m_lines[j];
         block += '\n';
     }
-    // p.set_cache(&m_cache);
-    m_thread_busy = true;
     m_thread_ptr.reset(new interruptible_thread([=]() {
                 try {
                     snapshot & s = i == 0 ? m_empty_snapshot : m_file->m_snapshots[i-1];
@@ -151,8 +147,8 @@ void server::process_from(unsigned linenum) {
                     scoped_updt_options updt(m_ios, s.m_options);
                     parser p(s.m_env, m_ios, strm, m_file->m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
                              &m_file->m_snapshots, &m_file->m_info);
+                    p.set_cache(&m_cache);
                     p();
-                    m_thread_busy  = false;
                     std::cout << "DONE\n";
                 } catch (exception& ex) {}
             }));
@@ -210,6 +206,8 @@ void server::replace_line(unsigned linenum, std::string const & new_line) {
     interrupt_thread();
     check_file();
     m_file->replace_line(linenum, new_line);
+    reset_thread();
+    m_file->m_info.invalidate_line(linenum+1);
     process_from(linenum);
 }
 
@@ -217,6 +215,8 @@ void server::insert_line(unsigned linenum, std::string const & new_line) {
     interrupt_thread();
     check_file();
     m_file->insert_line(linenum, new_line);
+    reset_thread();
+    m_file->m_info.insert_line(linenum+1);
     process_from(linenum);
 }
 
@@ -224,6 +224,8 @@ void server::remove_line(unsigned linenum) {
     interrupt_thread();
     check_file();
     m_file->remove_line(linenum);
+    reset_thread();
+    m_file->m_info.remove_line(linenum+1);
     process_from(linenum);
 }
 
@@ -254,7 +256,7 @@ void server::set_option(std::string const & line) {
 }
 
 void server::show_info(unsigned linenum) {
-    if (m_thread_busy) {
+    if (!m_file->m_info.is_available(linenum)) {
         m_out << "-- BEGININFO\n-- NAY\n-- ENDINFO" << std::endl;
         return;
     }
@@ -270,7 +272,7 @@ void server::show_info(unsigned linenum) {
 }
 
 void server::eval(std::string const & line) {
-    if (m_thread_busy) {
+    if (!m_file->m_info.is_available(m_file->m_lines.size())) {
         m_out << "-- BEGINEVAL\n-- NAY\n-- ENDEVAL" << std::endl;
         return;
     }
@@ -322,6 +324,11 @@ bool server::operator()(std::istream & in) {
             } else if (is_command(g_eval, line)) {
                 read_line(in, line);
                 eval(line);
+            } else if (is_command(g_wait, line)) {
+                if (m_thread_ptr) {
+                    m_thread_ptr->join();
+                    m_thread_ptr.reset(nullptr);
+                }
             } else {
                 throw exception(sstream() << "unexpected command line: " << line);
             }
diff --git a/src/frontends/lean/server.h b/src/frontends/lean/server.h
index c3361e6f2..e3397acd5 100644
--- a/src/frontends/lean/server.h
+++ b/src/frontends/lean/server.h
@@ -41,7 +41,6 @@ class server {
     unsigned                  m_num_threads;
     snapshot                  m_empty_snapshot;
     definition_cache          m_cache;
-    atomic<bool>              m_thread_busy;
     std::unique_ptr<interruptible_thread> m_thread_ptr;
 
     void load_file(std::string const & fname);
diff --git a/src/library/definition_cache.cpp b/src/library/definition_cache.cpp
index 15d004b14..324329231 100644
--- a/src/library/definition_cache.cpp
+++ b/src/library/definition_cache.cpp
@@ -145,6 +145,11 @@ void definition_cache::add(name const & n, expr const & pre_type, expr const & p
     add_core(n, pre_type, pre_value, ls, type, value);
 }
 
+void definition_cache::erase(name const & n) {
+    lock_guard<mutex> lc(m_mutex);
+    m_definitions.erase(n);
+}
+
 optional<std::tuple<level_param_names, expr, expr>> definition_cache::find(name const & n, expr const & pre_type, expr const & pre_value) {
     entry const * it;
     {
diff --git a/src/library/definition_cache.h b/src/library/definition_cache.h
index 3bd2a99f3..83e568f24 100644
--- a/src/library/definition_cache.h
+++ b/src/library/definition_cache.h
@@ -35,6 +35,6 @@ public:
     /** \brief Load the cache content from the given stream */
     void load(std::istream & in);
     /** \brief Remove the entry named \c n from the cache. */
-    void erase(name const & n) { m_definitions.erase(n); }
+    void erase(name const & n);
 };
 }
diff --git a/tests/lean/interactive/in1.input b/tests/lean/interactive/in1.input
new file mode 100644
index 000000000..d4cea72e8
--- /dev/null
+++ b/tests/lean/interactive/in1.input
@@ -0,0 +1,21 @@
+VISIT simple.lean
+WAIT
+INFO 4
+REPLACE 4
+definition foo {A B : Type} (a : A) (b : B) := b
+WAIT
+INFO 4
+INSERT 4
+
+WAIT
+INFO 5
+REMOVE 4
+WAIT
+INFO 4
+REPLACE 4
+defition foo {A B : Type} (a : A) (b : B) := b
+WAIT
+REPLACE 4
+definition foo {A B : Type} (a : A) (b : B) := b
+WAIT
+INFO 4
\ No newline at end of file
diff --git a/tests/lean/interactive/in1.input.expected.out b/tests/lean/interactive/in1.input.expected.out
new file mode 100644
index 000000000..b52ee7a53
--- /dev/null
+++ b/tests/lean/interactive/in1.input.expected.out
@@ -0,0 +1,63 @@
+DONE
+-- BEGININFO
+-- TYPE|4|33
+Type
+-- ACK
+-- TYPE|4|41
+Type
+-- ACK
+-- TYPE|4|47
+A
+-- ACK
+-- ENDINFO
+DONE
+-- BEGININFO
+-- TYPE|4|33
+Type
+-- ACK
+-- TYPE|4|41
+Type
+-- ACK
+-- TYPE|4|47
+B
+-- ACK
+-- ENDINFO
+DONE
+-- BEGININFO
+-- TYPE|5|33
+Type
+-- ACK
+-- TYPE|5|41
+Type
+-- ACK
+-- TYPE|5|47
+B
+-- ACK
+-- ENDINFO
+DONE
+-- BEGININFO
+-- TYPE|4|33
+Type
+-- ACK
+-- TYPE|4|41
+Type
+-- ACK
+-- TYPE|4|47
+B
+-- ACK
+-- ENDINFO
+simple.lean:4:0: error: command expected
+simple.lean:5:37: error: unknown identifier 'foo'
+DONE
+DONE
+-- BEGININFO
+-- TYPE|4|33
+Type
+-- ACK
+-- TYPE|4|41
+Type
+-- ACK
+-- TYPE|4|47
+B
+-- ACK
+-- ENDINFO
diff --git a/tests/lean/interactive/simple.lean b/tests/lean/interactive/simple.lean
new file mode 100644
index 000000000..7404c94b4
--- /dev/null
+++ b/tests/lean/interactive/simple.lean
@@ -0,0 +1,8 @@
+import standard
+
+namespace tst
+definition foo {A B : Type} (a : A) (b : B) := a
+definition boo {A : Type} (a : A) := foo a a
+end tst
+
+definition pr1 {A : Type} (a b : A) := a
\ No newline at end of file
diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
index 8e632559b..a91ecf409 100755
--- a/tests/lean/interactive/test_single.sh
+++ b/tests/lean/interactive/test_single.sh
@@ -12,7 +12,7 @@ else
 fi
 f=$2
 echo "-- testing $f"
-$LEAN -i < $f > $f.produced.out
+$LEAN --server < $f > $f.produced.out
 if test -f $f.expected.out; then
     if diff $f.produced.out $f.expected.out; then
         echo "-- checked"