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

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

Browse source 
m_theorem_queue.join() method assumes there are no open namespaces/scopes
This commit is contained in:
Leonardo de Moura 2014-12-05 16:12:23 -08:00
parent 1dc0790004
commit 53d6d76162
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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