michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/parser): do not generate error when 'exit' command is used

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-09 10:14:14 -08:00
parent 116e7ff82e
commit d67583df44
3 changed files with 22 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/parser.cpp
View file

@ -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()) {

17
src/library/scoped_ext.cpp
View file

@ -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);

9
src/library/scoped_ext.h
View file

@ -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) */