diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp index 94723ed87..f50e89543 100644 --- a/src/frontends/lean/dependencies.cpp +++ b/src/frontends/lean/dependencies.cpp @@ -12,43 +12,33 @@ Author: Leonardo de Moura #include "frontends/lean/scanner.h" namespace lean { -/** - \brief Keep scanning the input until finds an import or an Eof. - If \c import return true, otherwise return false -*/ -bool consume_until_import(environment const & env, scanner & s) { - name import("import"); - scanner::token_kind t; - while (true) { - try { - t = s.scan(env); - if (t == scanner::token_kind::Eof) - return false; - if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) - return true; - } catch (...) {} - } -} - void display_deps(environment const & env, std::ostream & out, char const * fname) { + name import("import"); std::ifstream in(fname); if (in.bad() || in.fail()) throw exception(sstream() << "failed to open file '" << fname << "'"); scanner s(in, fname); - while (consume_until_import(env, s)) { - while (true) { - auto t = s.scan(env); - if (t != scanner::token_kind::Identifier) - break; + bool import_args = false; + while (true) { + scanner::token_kind t; + try { + t = s.scan(env); + } catch (exception &) {} + if (t == scanner::token_kind::Eof) { + return; + } else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) { + import_args = true; + } else if (import_args == true && t == scanner::token_kind::Identifier) { std::string m_name = find_file(name_to_file(s.get_name_val()), {".lean", ".olean", ".lua"}); int last_idx = m_name.find_last_of("."); std::string rawname = m_name.substr(0, last_idx); std::string ext = m_name.substr(last_idx); - if (ext == ".lean") { + if (ext == ".lean") m_name = rawname + ".olean"; - } display_path(out, m_name); out << "\n"; + } else { + import_args = false; } } }