From d67583df442be75cd9769b3385c803ff3d9a0d37 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Dec 2014 10:14:14 -0800
Subject: [PATCH] fix(frontends/lean/parser): do not generate error when 'exit'
 command is used

---
 src/frontends/lean/parser.cpp |  3 ++-
 src/library/scoped_ext.cpp    | 17 ++++++++++++-----
 src/library/scoped_ext.h      |  9 ++++++++-
 3 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index f5478405f..ff51bb9db 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1434,7 +1434,8 @@ bool parser::parse_commands() {
                 throw_parser_exception("invalid end of module, expecting 'end'", pos());
         }
     } catch (interrupt_parser) {
-        display_error("parser has been interrupted", m_last_cmd_pos);
+        while (has_open_scopes(m_env))
+            m_env = pop_scope_core(m_env);
     }
     commit_info(m_scanner.get_line()+1);
     for (certified_declaration const & thm : m_theorem_queue.join()) {
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 856e3d5d9..c2d710065 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -147,13 +147,10 @@ static void namespace_reader(deserializer & d, module_idx, shared_environment &,
         });
 }
 
-environment pop_scope(environment const & env, name const & n) {
+environment pop_scope_core(environment const & env) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
-        throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
-    if (n != head(ext.m_headers))
-        throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
-                        << head(ext.m_headers) << "', and ends with '" << n << "'");
+        return env;
     scope_kind k      = head(ext.m_scope_kinds);
     ext.m_namespaces  = tail(ext.m_namespaces);
     ext.m_headers     = tail(ext.m_headers);
@@ -165,6 +162,16 @@ environment pop_scope(environment const & env, name const & n) {
     return r;
 }
 
+environment pop_scope(environment const & env, name const & n) {
+    scope_mng_ext ext = get_extension(env);
+    if (is_nil(ext.m_namespaces))
+        throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
+    if (n != head(ext.m_headers))
+        throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
+                        << head(ext.m_headers) << "', and ends with '" << n << "'");
+    return pop_scope_core(env);
+}
+
 bool has_open_scopes(environment const & env) {
     scope_mng_ext ext = get_extension(env);
     return !is_nil(ext.m_namespaces);
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index 1bf6c2ea0..ad000eb22 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -31,8 +31,15 @@ environment export_namespace(environment const & env, io_state const & ios, name
 
 /** \brief Create a new scope, all scoped extensions are notified. */
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n = name());
-/** \brief Delete the most recent scope, all scoped extensions are notified. */
+/** \brief Delete the most recent scope, all scoped extensions are notified.
+    \remark method throws an exception if there are no open scopes, or \c n does not match the name of the open scope
+*/
 environment pop_scope(environment const & env, name const & n = name());
+/** \brief Similar to \c pop_scope, but it always succeed.
+    It always pops the current open scope, and does nothing if there are no open scope.
+*/
+environment pop_scope_core(environment const & env);
+/** \brief Return true iff there are open scopes */
 bool has_open_scopes(environment const & env);
 
 /** \brief Add a new namespace (if it does not exist) */