From 53d6d7616216321ae64cf70187182c197f9acaba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Dec 2014 16:12:23 -0800 Subject: [PATCH] fix(frontends/lean/parser): generate error when 'exit' command is used m_theorem_queue.join() method assumes there are no open namespaces/scopes --- src/frontends/lean/parser.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 62bbe23603..f5478405f2 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1433,7 +1433,9 @@ bool parser::parse_commands() { else if (m_use_exceptions) throw_parser_exception("invalid end of module, expecting 'end'", pos()); } - } catch (interrupt_parser) {} + } catch (interrupt_parser) { + display_error("parser has been interrupted", m_last_cmd_pos); + } commit_info(m_scanner.get_line()+1); for (certified_declaration const & thm : m_theorem_queue.join()) { if (keep_new_thms())