diff --git a/doc/server.org b/doc/server.org
index e8163d8801..6916ebe6bc 100644
--- a/doc/server.org
+++ b/doc/server.org
@@ -30,7 +30,28 @@ REPLACE [line-number]
 This command replaces the line =[line-number]= with =[new-line]=.
 Lean uses the snapshots to process the request efficiently.
 If =[line-number]= is greater than the total number of lines in the lean
-buffer, then empty lines are introduced.
+buffer, then empty lines are introduced. The lines are indexed from 1.
+
+** Insert line
+
+#+BEGIN_SRC
+INSERT [line-number]
+[new-line]
+#+END_SRC
+
+This command inserts =[new-line]= before line =[line-number]=.
+If =[line-number]= is greater than the total number of lines in the lean
+buffer, then empty lines are introduced. The lines are indexed from 1.
+
+** Remove line
+
+#+BEGIN_SRC
+REMOVE [line-number]
+#+END_SRC
+
+Remove line =[line-number]=. The lines are indexed from 1.
+If =[line-number]= is greater than the total number of lines in the lean
+buffer, then the command is ignored.
 
 ** Extracting typing information
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index d41c6e7f45..12edf73a4c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1204,6 +1204,7 @@ bool parser::parse_commands() {
                 throw_parser_exception("invalid end of module, expecting 'end'", pos());
         }
     } catch (interrupt_parser) {}
+    save_snapshot();
     for (certified_declaration const & thm : m_theorem_queue.join()) {
         m_env.replace(thm);
     }
diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index cb530a1f4d..1ad570f885 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -6,17 +6,20 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <functional>
+#include "util/sstream.h"
 #include "frontends/lean/server.h"
 #include "frontends/lean/parser.h"
 
 namespace lean {
 server::server(environment const & env, io_state const & ios, unsigned num_threads):
     m_env(env), m_options(ios.get_options()), m_ios(ios), m_num_threads(num_threads),
-    m_empty_snapshot(m_env, m_options) {
+    m_empty_snapshot(m_env, m_options), m_from(0) {
 }
 
 static std::string g_file("FILE");
 static std::string g_replace("REPLACE");
+static std::string g_insert("INSERT");
+static std::string g_remove("REMOVE");
 static std::string g_info("INFO");
 
 static bool is_command(std::string const & cmd, std::string const & line) {
@@ -79,6 +82,13 @@ void server::process_from(unsigned linenum) {
     p();
 }
 
+void server::update() {
+    if (m_from == m_lines.size())
+        return;
+    process_from(m_from);
+    m_from = m_lines.size();
+}
+
 void server::read_file(std::string const & fname) {
     std::ifstream in(fname);
     if (in.bad() || in.fail()) {
@@ -89,7 +99,7 @@ void server::read_file(std::string const & fname) {
         for (std::string line; std::getline(in, line);) {
             m_lines.push_back(line);
         }
-        process_from(0);
+        m_from = 0;
     }
 }
 
@@ -97,10 +107,38 @@ void server::replace_line(unsigned linenum, std::string const & new_line) {
     while (linenum >= m_lines.size())
         m_lines.push_back("");
     m_lines[linenum] = new_line;
-    process_from(linenum);
+    if (linenum < m_from)
+        m_from = linenum;
+}
+
+void server::insert_line(unsigned linenum, std::string const & new_line) {
+    while (linenum >= m_lines.size())
+        m_lines.push_back("");
+    m_lines.push_back("");
+    lean_assert(m_lines.size() >= linenum+1);
+    unsigned i = m_lines.size();
+    while (i > linenum) {
+        --i;
+        m_lines[i] = m_lines[i-1];
+    }
+    m_lines[linenum] = new_line;
+    if (linenum < m_from)
+        m_from = linenum;
+}
+
+void server::remove_line(unsigned linenum) {
+    if (linenum >= m_lines.size())
+        return;
+    lean_assert(!m_lines.empty());
+    for (unsigned i = linenum; i < m_lines.size()-1; i++)
+        m_lines[i] = m_lines[i+1];
+    m_lines.pop_back();
+    if (linenum < m_from)
+        m_from = linenum;
 }
 
 void server::show_info(unsigned linenum) {
+    update();
     unsigned i = find(linenum);
     environment const & env = i == 0 ? m_env     : m_snapshots[i-1].m_env;
     options const & o       = i == 0 ? m_options : m_snapshots[i-1].m_options;
@@ -110,29 +148,47 @@ void server::show_info(unsigned linenum) {
     out << "-- ENDINFO" << endl;
 }
 
+void server::read_line(std::istream & in, std::string & line) {
+    if (!std::getline(in, line))
+        throw exception("unexpected end of input");
+}
+
+// Given a line of the form "cmd linenum", return the linenum
+unsigned server::get_linenum(std::string const & line, std::string const & cmd) {
+    std::string data = line.substr(cmd.size());
+    trim(data);
+    unsigned r = atoi(data.c_str());
+    if (r == 0)
+        throw exception("line numbers are indexed from 1");
+    return r;
+}
+
 bool server::operator()(std::istream & in) {
     for (std::string line; std::getline(in, line);) {
-        if (is_command(g_file, line)) {
-            std::string fname = line.substr(g_file.size());
-            trim(fname);
-            read_file(fname);
-        } else if (is_command(g_replace, line)) {
-            std::string data = line.substr(g_replace.size());
-            trim(data);
-            unsigned linenum = atoi(data.c_str());
-            if (std::getline(in, line)) {
-                replace_line(linenum, line);
+        try {
+            if (is_command(g_file, line)) {
+                std::string fname = line.substr(g_file.size());
+                trim(fname);
+                read_file(fname);
+            } else if (is_command(g_replace, line)) {
+                unsigned linenum = get_linenum(line, g_replace);
+                read_line(in, line);
+                replace_line(linenum-1, line);
+            } else if (is_command(g_insert, line)) {
+                unsigned linenum = get_linenum(line, g_replace);
+                read_line(in, line);
+                insert_line(linenum-1, line);
+            } else if (is_command(g_remove, line)) {
+                unsigned linenum = get_linenum(line, g_replace);
+                remove_line(linenum-1);
+            } else if (is_command(g_info, line)) {
+                unsigned linenum = get_linenum(line, g_info);
+                show_info(linenum);
             } else {
-                std::cout << "Error: unexpected end of input\n";
-                return false;
+                throw exception(sstream() << "unexpected command line: " << line);
             }
-        } else if (is_command(g_info, line)) {
-            std::string data = line.substr(g_info.size());
-            trim(data);
-            unsigned linenum = atoi(data.c_str());
-            show_info(linenum);
-        } else {
-            std::cout << "Error: unexpected command line: " << line << "\n";
+        } catch (exception & ex) {
+            std::cout << "Error: " << ex.what() << "\n";
         }
     }
     return true;
diff --git a/src/frontends/lean/server.h b/src/frontends/lean/server.h
index c12a5d080d..56692d512d 100644
--- a/src/frontends/lean/server.h
+++ b/src/frontends/lean/server.h
@@ -25,12 +25,18 @@ class server {
     unsigned                  m_num_threads;
     snapshot                  m_empty_snapshot;
     std::string               m_fname;
+    unsigned                  m_from;
 
     void read_file(std::string const & fname);
     void replace_line(unsigned linenum, std::string const & new_line);
+    void insert_line(unsigned linenum, std::string const & new_line);
+    void remove_line(unsigned linenum);
     void show_info(unsigned linenum);
     void process_from(unsigned linenum);
     unsigned find(unsigned linenum);
+    void update();
+    void read_line(std::istream & in, std::string & line);
+    unsigned get_linenum(std::string const & line, std::string const & cmd);
 
 public:
     server(environment const & env, io_state const & ios, unsigned num_threads = 1);