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

fix(frontends/lean/server): do not fail if file does not exist in 'VISIT file'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-06 12:34:20 -07:00
parent 5549295c47
commit 87d7391d7a
2 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/server.cpp
View file

@ -303,11 +303,16 @@ void server::process_from(unsigned line_num) {
m_worker.set_todo(m_file, line_num, m_ios.get_options());
}
void server::load_file(std::string const & fname) {
void server::load_file(std::string const & fname, bool error_if_nofile) {
interrupt_worker();
std::ifstream in(fname);
if (in.bad() || in.fail()) {
m_out << "-- ERROR failed to open file '" << fname << "'" << std::endl;
if (error_if_nofile) {
m_out << "-- ERROR failed to open file '" << fname << "'" << std::endl;
} else {
m_file.reset(new file(in, fname));
m_file_map.insert(mk_pair(fname, m_file));
}
} else {
m_file.reset(new file(in, fname));
m_file_map.insert(mk_pair(fname, m_file));
@ -319,7 +324,8 @@ void server::visit_file(std::string const & fname) {
interrupt_worker();
auto it = m_file_map.find(fname);
if (it == m_file_map.end()) {
load_file(fname);
bool error_if_nofile = false;
load_file(fname, error_if_nofile);
} else {
m_file = it->second;
process_from(0);

2
src/frontends/lean/server.h
View file

@ -70,7 +70,7 @@ class server {
definition_cache m_cache;
worker m_worker;
void load_file(std::string const & fname);
void load_file(std::string const & fname, bool error_if_nofile = true);
void visit_file(std::string const & fname);
void check_file();
void replace_line(unsigned line_num, std::string const & new_line);