feat(frontends/lean): only valid proof states should be displayed, closes #275

src/frontends/lean/decl_cmds.cpp

@@ -442,6 +442,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
     }
 
     if (!found_cached) {
+        p.remove_proof_state_info(n_pos, p.pos());
         if (is_theorem) {
             auto type_pos = p.pos_of(type);
             bool clear_pre_info = false; // we don't want to clear pre_info data until we process the proof.

src/frontends/lean/info_manager.cpp

@@ -69,6 +69,7 @@ public:
     bool is_cheap() const { return m_ptr->is_cheap(); }
     void display(io_state_stream const & ios, unsigned line) const { m_ptr->display(ios, line); }
     info_data_cell const * raw() const { return m_ptr; }
+    info_kind kind() const { return m_ptr->kind(); }
 };
 
 struct tmp_info_data : public info_data_cell {
@@ -444,6 +445,30 @@ struct info_manager::imp {
         m_line_data[l].insert(mk_proof_state_info(c, ps));
     }
 
+    void remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col) {
+        lock_guard<mutex> lc(m_mutex);
+        if (m_block_new_info || m_line_data.empty())
+            return;
+        if (end_line >= m_line_data.size())
+            end_line = m_line_data.size() - 1;
+        for (unsigned i = start_line; i <= end_line; i++) {
+            info_data_set const & curr_set = m_line_data[i];
+            if (curr_set.find_if([](info_data const & info) { return info.kind() == info_kind::ProofState; })) {
+                info_data_set new_curr_set;
+                curr_set.for_each([&](info_data const & info) {
+                        if (info.kind() == info_kind::ProofState) {
+                            if ((i == start_line && info.get_column() < start_col) ||
+                                (i == end_line && info.get_column() >= end_col))
+                                new_curr_set.insert(info);
+                        } else {
+                            new_curr_set.insert(info);
+                        }
+                    });
+                m_line_data[i] = new_curr_set;
+            }
+        }
+    }
+
     static info_data_set instantiate(info_data_set const & s, substitution & subst) {
         info_data_set r;
         s.for_each([&](info_data const & d) {
@@ -724,4 +749,7 @@ optional<expr> info_manager::get_type_at(unsigned line, unsigned col) const { re
 optional<expr> info_manager::get_meta_at(unsigned line, unsigned col) const { return m_ptr->get_meta_at(line, col); }
 void info_manager::block_new_info() { m_ptr->block_new_info(true); }
 void info_manager::start_from(unsigned l) { m_ptr->start_from(l); }
+void info_manager::remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col) {
+    m_ptr->remove_proof_state_info(start_line, start_col, end_line, end_col);
+}
 }

src/frontends/lean/info_manager.h

@@ -30,6 +30,9 @@ public:
     void add_identifier_info(unsigned l, unsigned c, name const & full_id);
     void add_proof_state_info(unsigned l, unsigned c, proof_state const & e);
 
+    /** \brief Remove PROO_STATE info from [(start_line, start_line), (end_line, end_col)) */
+    void remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col);
+
     void instantiate(substitution const & s);
 
     void merge(info_manager const & m, bool overwrite);

src/frontends/lean/parser.cpp

@@ -164,6 +164,11 @@ bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const
     return true;
 }
 
+void parser::remove_proof_state_info(pos_info const & start, pos_info const & end) {
+    if (m_info_manager)
+        m_info_manager->remove_proof_state_info(start.first, start.second, end.first, end.second);
+}
+
 expr parser::mk_sorry(pos_info const & p) {
     m_used_sorry = true;
     {

src/frontends/lean/parser.h

@@ -226,6 +226,7 @@ public:
 
     bool are_info_lines_valid(unsigned start_line, unsigned end_line) const;
     bool collecting_info() const { return m_info_manager; }
+    void remove_proof_state_info(pos_info const & start, pos_info const & end);
 
     void set_index(declaration_index * i) { m_index = i; }
     void add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t);