diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index cf7408bce..567d355cd 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -232,12 +232,20 @@ void server::worker::request_interrupt() {
     m_thread.request_interrupt();
 }
 
-void server::worker::wait() {
+bool server::worker::wait(optional<unsigned> const & ms) {
     while (true) {
         unique_lock<mutex> lk(m_todo_mutex);
         if (!m_todo_file)
-            break;
-        m_todo_cv.wait(lk);
+            return true;
+        if (ms) {
+            chrono::milliseconds d(*ms);
+            m_todo_cv.wait_for(lk, d);
+            if (!m_todo_file)
+                return true;
+            return false;
+        } else {
+            m_todo_cv.wait(lk);
+        }
     }
 }
 
@@ -361,6 +369,16 @@ unsigned consume_num(std::string const & data, unsigned & i) {
     return r;
 }
 
+optional<unsigned> server::get_optional_num(std::string const & line, std::string const & cmd) {
+    std::string data = line.substr(cmd.size());
+    unsigned i = 0;
+    consume_spaces(data, i);
+    if (i == data.size())
+        return optional<unsigned>();
+    unsigned r = consume_num(data, i);
+    return optional<unsigned>(r);
+}
+
 void check_line_num(unsigned line_num) {
     if (line_num == 0)
         throw exception("line numbers are indexed from 1");
@@ -740,6 +758,13 @@ void server::find_goal_matches(unsigned line_num, unsigned col_num, std::string
     m_out << "-- ENDFINDG" << std::endl;
 }
 
+void server::wait(optional<unsigned> ms) {
+    m_out << "-- BEGINWAIT" << std::endl;
+    if (!m_worker.wait(ms))
+        m_out << "-- INTERRUPTED\n";
+    m_out << "-- ENDWAIT" << std::endl;
+}
+
 bool server::operator()(std::istream & in) {
     for (std::string line; std::getline(in, line);) {
         try {
@@ -779,9 +804,8 @@ bool server::operator()(std::istream & in) {
             } else if (is_command(g_options, line)) {
                 show_options();
             } else if (is_command(g_wait, line)) {
-                m_out << "-- BEGINWAIT" << std::endl;
-                m_worker.wait();
-                m_out << "-- ENDWAIT" << std::endl;
+                optional<unsigned> ms = get_optional_num(line, g_wait);
+                wait(ms);
             } else if (is_command(g_show, line)) {
                 show(false);
             } else if (is_command(g_valid, line)) {
diff --git a/src/frontends/lean/server.h b/src/frontends/lean/server.h
index fdf3c9496..00ca5f512 100644
--- a/src/frontends/lean/server.h
+++ b/src/frontends/lean/server.h
@@ -57,7 +57,7 @@ class server {
         ~worker();
         void set_todo(file_ptr const & f, unsigned line_num, options const & o);
         void request_interrupt();
-        void wait();
+        bool wait(optional<unsigned> const & ms);
     };
 
     file_map                  m_file_map;
@@ -89,7 +89,9 @@ class server {
     void interrupt_worker();
     void show_options();
     void show(bool valid);
+    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);
     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);