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

feat(frontends/lean/parser): allow parser to continue even if there are errors importing files

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-14 11:02:07 -07:00
parent 0d97fff280
commit 8afd433f34
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1180,7 +1180,10 @@ bool parser::parse_commands() {
scoped_set_distinguishing_pp_options set(get_distinguishing_pp_options());
try {
bool done = false;
protected_call([&]() {
parse_imports();
},
[&]() { sync_command(); });
if (has_sorry(m_env)) {
flycheck_warning wrn(regular_stream());
display_warning_pos(pos());