diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h
index 021d1b5f5c..841529d9f8 100644
--- a/src/frontends/lean/info_manager.h
+++ b/src/frontends/lean/info_manager.h
@@ -110,6 +110,7 @@ public:
     void add_hole_info(pos_info const & begin_pos, pos_info const & end_pos, tactic_state const & s, expr const & hole_args);
 
     line_info_data_set get_line_info_set(unsigned l) const;
+    rb_map<unsigned, line_info_data_set, unsigned_cmp> const & get_line_info_sets() const { return m_line_data; }
 
     void instantiate_mvars(metavar_context const & mctx);
     void merge(info_manager const & info);
diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp
index 1afe434f01..93224c1970 100644
--- a/src/frontends/lean/interactive.cpp
+++ b/src/frontends/lean/interactive.cpp
@@ -255,18 +255,11 @@ bool execute_hole_command(tactic_state const & s, name const & cmd_decl_name, ex
     }
 }
 
-void get_hole_commands(module_info const & m_mod_info,
-                       std::vector<info_manager> const & info_managers,
-                       pos_info const & pos, json & j) {
-    optional<info_data> info = find_hole(m_mod_info, info_managers, pos);
-    if (!info)
-        throw exception("hole not found");
-    hole_info_data const & hole = to_hole_info_data(*info);
+bool json_of_hole(hole_info_data const & hole, std::string const & file, json & j) {
     tactic_state const & s = hole.get_tactic_state();
     buffer<pair<name, std::string>> cmd_descrs;
     get_hole_commands(s.env(), cmd_descrs);
-    if (cmd_descrs.empty())
-        throw exception("hole commands are not available");
+    if (cmd_descrs.empty()) return false;
     std::vector<json> ds;
     for (auto const & p : cmd_descrs) {
         json d;
@@ -275,11 +268,47 @@ void get_hole_commands(module_info const & m_mod_info,
         ds.push_back(d);
     }
     j["results"] = ds;
-    j["file"] = m_mod_info.m_mod;
+    j["file"] = file;
     j["start"]["line"]   = hole.get_begin_pos().first;
     j["start"]["column"] = hole.get_begin_pos().second;
     j["end"]["line"]     = hole.get_end_pos().first;
     j["end"]["column"]   = hole.get_end_pos().second;
+    return true;
+}
+
+void get_hole_commands(module_info const & m_mod_info,
+                       std::vector<info_manager> const & info_managers,
+                       pos_info const & pos, json & j) {
+    optional<info_data> info = find_hole(m_mod_info, info_managers, pos);
+    if (!info)
+        throw exception("hole not found");
+    hole_info_data const & hole = to_hole_info_data(*info);
+    if (!json_of_hole(hole, m_mod_info.m_mod, j)) {
+        throw exception("hole commands are not available");
+    }
+}
+
+void get_all_hole_commands(module_info const & m_mod_info,
+                           std::vector<info_manager> const & info_managers,
+                           json & j) {
+    std::vector<json> holes;
+    for (auto & infom : info_managers) {
+        if (infom.get_file_name() == m_mod_info.m_mod) {
+            infom.get_line_info_sets().for_each([&](unsigned, line_info_data_set const & S) {
+                S.for_each([&](unsigned, list<info_data> const & info_list) {
+                    for (info_data const & info : info_list) {
+                        if (hole_info_data const * hole = is_hole_info_data(info)) {
+                            json j;
+                            if (json_of_hole(*hole, m_mod_info.m_mod, j)) {
+                                holes.push_back(j);
+                            }
+                        }
+                    }
+                });
+            });
+        }
+    }
+    j["holes"] = holes;
 }
 
 void execute_hole_command(module_info const & m_mod_info,
diff --git a/src/frontends/lean/interactive.h b/src/frontends/lean/interactive.h
index e8da2b6e1c..44b130c00f 100644
--- a/src/frontends/lean/interactive.h
+++ b/src/frontends/lean/interactive.h
@@ -21,6 +21,9 @@ void report_info(environment const & env, options const & opts, io_state const &
 void get_hole_commands(module_info const & m_mod_info,
                        std::vector<info_manager> const & info_managers,
                        pos_info const & pos, json & j);
+void get_all_hole_commands(module_info const & m_mod_info,
+                           std::vector<info_manager> const & info_managers,
+                           json & j);
 void execute_hole_command(module_info const & m_mod_info,
                           std::vector<info_manager> const & info_managers,
                           pos_info const & pos, std::string const & action, json & j);
diff --git a/src/shell/server.cpp b/src/shell/server.cpp
index 6f0fadfbad..1e6d7fcbd4 100644
--- a/src/shell/server.cpp
+++ b/src/shell/server.cpp
@@ -441,6 +441,8 @@ void server::handle_request(server::cmd_req const & req) {
         handle_async_response(req, handle_hole(req));
     } else if (command == "hole_commands") {
         send_msg(handle_hole_commands(req));
+    } else if (command == "all_hole_commands") {
+        send_msg(handle_all_hole_commands(req));
     } else if (command == "search") {
         send_msg(handle_search(req));
     } else if (command == "roi") {
@@ -653,6 +655,15 @@ server::cmd_res server::handle_hole_commands(server::cmd_req const & req) {
     return cmd_res(req.m_seq_num, j);
 }
 
+server::cmd_res server::handle_all_hole_commands(server::cmd_req const & req) {
+    std::string fn     = req.m_payload.at("file_name");
+    auto mod_info      = m_mod_mgr->get_module(fn);
+    std::vector<info_manager> im = get_info_managers(m_lt);
+    json j;
+    get_all_hole_commands(*mod_info, im, j);
+    return cmd_res(req.m_seq_num, j);
+}
+
 server::cmd_res server::handle_search(server::cmd_req const & req) {
     std::string query = req.m_payload.at("query");
 
diff --git a/src/shell/server.h b/src/shell/server.h
index c830f9ffff..ac782a53d2 100644
--- a/src/shell/server.h
+++ b/src/shell/server.h
@@ -99,6 +99,7 @@ class server : public module_vfs {
     task<cmd_res> handle_info(cmd_req const & req);
     task<cmd_res> handle_hole(cmd_req const & req);
     cmd_res handle_hole_commands(cmd_req const & req);
+    cmd_res handle_all_hole_commands(cmd_req const & req);
     cmd_res handle_search(cmd_req const & req);
     cmd_res handle_roi(cmd_req const & req);