max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(shell/completion): remove duplicate completion candidates

Browse source 
VS Code does not automatically remove them
This commit is contained in:
Sebastian Ullrich 2017-01-10 21:15:40 +01:00 • committed by Leonardo de Moura
parent 00c89f209c
commit 82bcdebf7c
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/shell/completion.cpp
View file

@ -73,6 +73,10 @@ void filter_completions(std::string const & pattern, std::vector<pair<std::strin
completions.push_back(serialize(selected[0].second));
} else if (sz > 1) {
std::sort(selected.begin(), selected.end());
auto it = std::unique(selected.begin(), selected.end(), [](pair<std::string, T> const & s1, pair<std::string, T> const & s2) {
return s1.first == s2.first;
});
selected.resize(it - selected.begin());
std::vector<pair<std::string, T>> next_selected;
auto process = [&](pair<std::string, T> const & s, bool select) {
if (select) {