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

fix(frontends/lean/info_manager): add missing method

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-14 10:53:22 -07:00
parent 99e77db8ad
commit d1c645977d
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/frontends/lean/info_manager.cpp
View file

@ -132,7 +132,18 @@ void info_manager::append(std::vector<std::unique_ptr<info_data>> && vs, bool re
}
}
void info_manager::append(std::vector<type_info_data> & v, bool remove_duplicates) {
void info_manager::append(std::vector<type_info_data> & vs, bool remove_duplicates) {
lock_guard<mutex> lc(m_mutex);
std::stable_sort(vs.begin(), vs.end());
type_info_data prev;
bool first = true;
for (auto & v : vs) {
if (!remove_duplicates || first || !v.eq_pos(prev.get_line(), prev.get_column())) {
prev = v;
add_core(std::unique_ptr<info_data>(new type_info_data(v)));
first = false;
}
}
}
void info_manager::sort() {