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

fix(frontends/lean/parser): generate flycheck-friendly import error

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-31 19:03:54 -07:00
parent 6ca80b5000
commit c01b4bd636
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1067,6 +1067,13 @@ void parser::parse_imports() {
} else if (auto it = find_file(f, ".olean")) {
olean_files.push_back(f);
} else {
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();