From 8afd433f346365e4ad272f6bb9b7746fb2269ed1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Aug 2014 11:02:07 -0700 Subject: [PATCH] feat(frontends/lean/parser): allow parser to continue even if there are errors importing files Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f03c114dc..59d916359 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1180,7 +1180,10 @@ bool parser::parse_commands() { scoped_set_distinguishing_pp_options set(get_distinguishing_pp_options()); try { bool done = false; - parse_imports(); + protected_call([&]() { + parse_imports(); + }, + [&]() { sync_command(); }); if (has_sorry(m_env)) { flycheck_warning wrn(regular_stream()); display_warning_pos(pos());