feat(frontends/lean/server): add SYNC command, closes #199

doc/server.org

@@ -34,6 +34,18 @@ apply "changes" to the current file. The =LOAD= command can be used to
 discard all these changes, and enforce the content of the file stored
 in file system.
 
+** Synchronize
+
+The following command can be used to make sure the front-end application
+and lean have the same "view". It resets the contents associated with current visited file/buffer.
+
+#+BEGIN_SRC
+SYNC [num]
+line_1
+...
+line_num
+#+END_SRC
+
 ** Replace line
 
 #+BEGIN_SRC

src/frontends/lean/info_manager.cpp

@@ -607,10 +607,11 @@ struct info_manager::imp {
 
     void clear() {
         lock_guard<mutex> lc(m_mutex);
-        if (m_block_new_info)
-            return;
         m_line_data.clear();
         m_line_valid.clear();
+        m_env_info.clear();
+        m_iteration      = 0;
+        m_processed_upto = 0;
     }
 };
 

src/frontends/lean/server.cpp

@@ -107,6 +107,13 @@ void server::file::show(std::ostream & out, bool valid) {
     }
 }
 
+void server::file::sync(std::vector<std::string> const & lines) {
+    lock_guard<mutex> lk(m_lines_mutex);
+    m_info.block_new_info();
+    m_info.clear();
+    m_lines = lines;
+}
+
 /**
    \brief Return index i <= m_snapshots.size() s.t.
       * forall j < i, m_snapshots[j].m_line < line
@@ -278,6 +285,7 @@ void server::interrupt_worker() {
 
 static std::string g_load("LOAD");
 static std::string g_visit("VISIT");
+static std::string g_sync("SYNC");
 static std::string g_replace("REPLACE");
 static std::string g_insert("INSERT");
 static std::string g_remove("REMOVE");
@@ -383,6 +391,13 @@ optional<unsigned> server::get_optional_num(std::string const & line, std::strin
     return optional<unsigned>(r);
 }
 
+unsigned server::get_num(std::string const & line, std::string const & cmd) {
+    if (auto r = get_optional_num(line, cmd))
+        return *r;
+    else
+        throw exception("numeral expected");
+}
+
 void check_line_num(unsigned line_num) {
     if (line_num == 0)
         throw exception("line numbers are indexed from 1");
@@ -424,6 +439,13 @@ void server::check_file() {
         throw exception("no file has been loaded/visited");
 }
 
+void server::sync(std::vector<std::string> const & lines) {
+    interrupt_worker();
+    check_file();
+    m_file->sync(lines);
+    process_from(0);
+}
+
 void server::replace_line(unsigned line_num, std::string const & new_line) {
     interrupt_worker();
     check_file();
@@ -786,6 +808,14 @@ bool server::operator()(std::istream & in) {
                 std::string fname = line.substr(g_visit.size());
                 trim(fname);
                 visit_file(fname);
+            } else if (is_command(g_sync, line)) {
+                unsigned nlines = get_num(line, g_sync);
+                std::vector<std::string> lines;
+                for (unsigned i = 0; i < nlines; i++) {
+                    read_line(in, line);
+                    lines.push_back(line);
+                }
+                sync(lines);
             } else if (is_command(g_echo, line)) {
                 std::string str = line.substr(g_echo.size());
                 m_out << "--" << str << "\n";

src/frontends/lean/server.h

@@ -38,6 +38,7 @@ class server {
         void show(std::ostream & out, bool valid);
         std::string const & get_fname() const { return m_fname; }
         info_manager const & infom() const { return m_info; }
+        void sync(std::vector<std::string> const & lines);
     };
     typedef std::shared_ptr<file>                     file_ptr;
     typedef std::unordered_map<std::string, file_ptr> file_map;
@@ -89,9 +90,11 @@ class server {
     void interrupt_worker();
     void show_options();
     void show(bool valid);
+    void sync(std::vector<std::string> const & lines);
     void wait(optional<unsigned> ms);
     unsigned get_line_num(std::string const & line, std::string const & cmd);
     optional<unsigned> get_optional_num(std::string const & line, std::string const & cmd);
+    unsigned get_num(std::string const & line, std::string const & cmd);
     pair<unsigned, optional<unsigned>> get_line_opt_col_num(std::string const & line, std::string const & cmd);
     pair<unsigned, unsigned> get_line_col_num(std::string const & line, std::string const & cmd);
     void find_goal_matches(unsigned line_num, unsigned col_num, std::string const & filters);

tests/lean/interactive/sync.input

@@ -0,0 +1,10 @@
+SET
+pp.notation false
+VISIT simple.lean
+WAIT
+SYNC 3
+import logic
+definition id {A : Type} (a : A) := a
+definition pr2 {A : Type} (a b : A) := b
+WAIT
+INFO 3

tests/lean/interactive/sync.input.expected.out

@@ -0,0 +1,23 @@
+-- BEGINSET
+-- ENDSET
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- SYMBOL|3|20
+Type
+-- ACK
+-- TYPE|3|33
+Type
+-- ACK
+-- IDENTIFIER|3|33
+A
+-- ACK
+-- TYPE|3|39
+A
+-- ACK
+-- IDENTIFIER|3|39
+b
+-- ACK
+-- ENDINFO