diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 9706d2e890..362ae622c6 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -15,7 +15,7 @@
     "context" "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
-    "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
+    "infix" "infixl" "infixr" "notation" "eval" "check" "coercion" "end"
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "add_rewrite" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing")
@@ -141,6 +141,7 @@
      (,(rx word-start (group "Type") ".") (1 'font-lock-type-face))
      ;; sorry
      (,(rx word-start "sorry" word-end) . 'font-lock-warning-face)
+     (,(rx word-start "exit" word-end) . 'font-lock-warning-face)
      ;; extra-keywords
      (,(rx (or "∎")) . 'font-lock-keyword-face)
      ;; lean-keywords
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index b5fc8270d7..e36dbc170f 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -382,7 +382,10 @@ environment eval_cmd(parser & p) {
     return p.env();
 }
 
-environment exit_cmd(parser &) {
+environment exit_cmd(parser & p) {
+    flycheck_warning wrn(p.regular_stream());
+    p.display_warning_pos(p.cmd_pos());
+    p.regular_stream() << " using 'exit' to interrupt Lean" << endl;
     throw interrupt_parser();
 }
 
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 85abc46f75..3d2e33b746 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -141,7 +141,6 @@ class parser {
     bool                   m_profile;
 
     void display_warning_pos(unsigned line, unsigned pos);
-    void display_warning_pos(pos_info p);
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
     void display_error(char const * msg, unsigned line, unsigned pos);
@@ -461,6 +460,7 @@ public:
 
     parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }
     void display_information_pos(pos_info p);
+    void display_warning_pos(pos_info p);
 
     /** return true iff profiling is enabled */
     bool profiling() const { return m_profile; }