diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 55004d234f..9e3ce80564 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -5,6 +5,6 @@ notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmds.cpp dependencies.cpp
 pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp decl_attributes.cpp
-opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
+prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp)
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2fe15496a3..d23410d289 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -46,7 +46,6 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/compiler.h"
 #include "library/equations_compiler/util.h"
 #include "frontends/lean/builtin_exprs.h"
-#include "frontends/lean/opt_cmd.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/elaborator.h"
diff --git a/src/frontends/lean/opt_cmd.cpp b/src/frontends/lean/opt_cmd.cpp
deleted file mode 100644
index 8147a7f2c6..0000000000
--- a/src/frontends/lean/opt_cmd.cpp
+++ /dev/null
@@ -1,49 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "frontends/lean/opt_cmd.h"
-
-namespace lean {
-static options set_line_col(options const & _opts, unsigned line, unsigned col) {
-    options opts = _opts;
-    opts = opts.update(name("line"), line);
-    opts = opts.update(name("column"), col);
-    return opts;
-}
-
-static bool has_show(options const & opts, name const & kind, unsigned & line, unsigned & col) {
-    if (opts.get_bool(kind)) {
-        line = opts.get_unsigned("line", 0);
-        col  = opts.get_unsigned("column", 0);
-        return true;
-    } else {
-        return false;
-    }
-}
-
-options set_show_goal(options const & opts, unsigned line, unsigned col) {
-    return set_line_col(opts.update(name("show_goal"), true), line, col);
-}
-
-bool has_show_goal(options const & opts, unsigned & line, unsigned & col) {
-    return has_show(opts, "show_goal", line, col);
-}
-
-options set_show_info(options const & opts, unsigned line, unsigned col) {
-    return set_line_col(opts.update(name("show_info"), true), line, col);
-}
-
-bool has_show_info(options const & opts, unsigned & line, unsigned & col) {
-    return has_show(opts, "show_info", line, col);
-}
-
-void print_lean_info_header(std::ostream & out) {
-    out << "LEAN_INFORMATION\n";
-}
-void print_lean_info_footer(std::ostream & out) {
-    out << "END_LEAN_INFORMATION\n";
-}
-}
diff --git a/src/frontends/lean/opt_cmd.h b/src/frontends/lean/opt_cmd.h
deleted file mode 100644
index cd84d0647a..0000000000
--- a/src/frontends/lean/opt_cmd.h
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/sexpr/options.h"
-
-namespace lean {
-// We use options to communicate auxiliary commands set by the lean.exe frontend.
-
-options set_show_goal(options const & opts, unsigned line, unsigned col);
-bool has_show_goal(options const & opts, unsigned & line, unsigned & col);
-
-options set_show_info(options const & opts, unsigned line, unsigned col);
-bool has_show_info(options const & opts, unsigned & line, unsigned & col);
-
-void print_lean_info_header(std::ostream & out);
-void print_lean_info_footer(std::ostream & out);
-}
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index b24b2b397f..af52cd789c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -56,7 +56,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/parser_pos_provider.h"
 #include "frontends/lean/update_environment_exception.h"
-#include "frontends/lean/opt_cmd.h"
 #include "frontends/lean/builtin_cmds.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/elaborator.h"
@@ -149,21 +148,6 @@ parser::all_id_local_scope::all_id_local_scope(parser & p):
 
 static name * g_tmp_prefix = nullptr;
 
-void parser::enable_show_goal(pos_info const & pos) {
-    m_stop_at = true;
-    m_stop_at_line = pos.first;
-    m_ios.set_options(set_show_goal(m_ios.get_options(), pos.first, pos.second));
-}
-
-void parser::enable_show_info(pos_info const & pos) {
-    m_stop_at = true;
-    m_stop_at_line = pos.first;
-    m_info_at = true;
-    m_info_at_line = pos.first;
-    m_info_at_col = pos.second;
-    m_ios.set_options(set_show_info(m_ios.get_options(), pos.first, pos.second));
-}
-
 parser::parser(environment const & env, io_state const & ios,
                module_loader const & import_fn,
                std::istream & strm, std::string const & file_name,
@@ -198,8 +182,6 @@ parser::parser(environment const & env, io_state const & ios,
     m_id_behavior  = id_behavior::ErrorIfUndef;
     m_found_errors = false;
     m_used_sorry   = false;
-    m_info_at = false;
-    m_stop_at = false;
     updt_options();
     m_next_tag_idx  = 0;
     m_curr = scanner::token_kind::Identifier;
@@ -2203,9 +2185,6 @@ bool parser::parse_commands() {
         }
         while (!done) {
             save_snapshot(scope_parser_msgs);
-            if (m_stop_at && pos().first > m_stop_at_line) {
-                throw interrupt_parser();
-            }
             scoped_task_context scope_task_ctx(get_current_module(), pos());
             scope_message_context scope_msg_ctx;
             // TODO(gabriel): separate flag for snapshots/infos?
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index ded163fb23..d40a427d49 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -150,13 +150,6 @@ class parser : public abstract_parser {
     // profiling
     bool                   m_profile;
 
-    // stop/info at line/col
-    bool                   m_stop_at; // if true, then parser stops execution after the given line and column is reached
-    unsigned               m_stop_at_line;
-    bool                   m_info_at;
-    unsigned               m_info_at_line;
-    unsigned               m_info_at_col;
-
     // If the following flag is true we do not raise error messages
     // noncomputable definitions not tagged as noncomputable.
     bool                   m_ignore_noncomputable;
@@ -241,8 +234,6 @@ public:
 
     void set_break_at_pos(pos_info const & pos) { m_break_at_pos = some(pos); }
     bool check_break_at_pos(pos_info const & p, name const & tk);
-    void enable_show_goal(pos_info const & pos);
-    void enable_show_info(pos_info const & pos);
 
     bool ignore_noncomputable() const { return m_ignore_noncomputable; }
     void set_ignore_noncomputable() { m_ignore_noncomputable = true; }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 7e992c265b..d891fa413f 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -40,7 +40,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/dependencies.h"
-#include "frontends/lean/opt_cmd.h"
 #include "frontends/smt2/parser.h"
 #include "frontends/lean/json.h"
 #include "library/native_compiler/options.h"