From c01b4bd6369277cbc9b5ab18a5ec40917902b258 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 31 Jul 2014 19:03:54 -0700 Subject: [PATCH] fix(frontends/lean/parser): generate flycheck-friendly import error Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index db04b962b..9d1b14c4d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1067,7 +1067,14 @@ void parser::parse_imports() { } else if (auto it = find_file(f, ".olean")) { olean_files.push_back(f); } else { - throw parser_error(sstream() << "invalid import, unknown module '" << f << "'", pos()); + m_found_errors = true; + if (!m_use_exceptions && m_show_errors) { + flycheck_error err(regular_stream()); + display_error_pos(pos()); + regular_stream() << " invalid import, unknown module '" << f << "'" << endl; + } + if (m_use_exceptions) + throw parser_error(sstream() << "invalid import, unknown module '" << f << "'", pos()); } next(); }