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

fix(frontends/lean/server): std::unordered_map::insert does replace

Browse source 
existing entry, fixes #188
This commit is contained in:
Leonardo de Moura 2014-09-12 16:47:56 -07:00
parent b7023ce1d8
commit 6db46e0505
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -324,10 +324,13 @@ void server::load_file(std::string const & fname, bool error_if_nofile) {
m_out << "-- ERROR failed to open file '" << fname << "'" << std::endl;
} else {
m_file.reset(new file(in, fname));
m_file_map.erase(fname);
m_file_map.insert(mk_pair(fname, m_file));
}
} else {
m_cache.clear();
m_file.reset(new file(in, fname));
m_file_map.erase(fname);
m_file_map.insert(mk_pair(fname, m_file));
process_from(0);
}