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

feat(shell/completion): only filter class projections

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-06 09:40:06 -08:00
parent 26e2aeec7a
commit 44ef2f4eeb
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/shell/completion.cpp
View file

@ -14,6 +14,7 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
#include "util/bitap_fuzzy_search.h"
#include "library/protected.h"
#include "library/scoped_ext.h"
#include "library/class.h"
#include "frontends/lean/util.h"
#include "util/lean_path.h"
@ -101,8 +102,11 @@ std::vector<json> get_decl_completions(std::string const & pattern, environment
std::vector<pair<std::string, name>> selected;
bitap_fuzzy_search matcher(pattern, max_errors);
env.for_each_declaration([&](declaration const & d) {
if (is_projection(env, d.get_name()))
return;
if (is_projection(env, d.get_name())) {
auto s_name = d.get_name().get_prefix();
if (is_class(env, s_name))
return;
}
if (auto it = exact_prefix_match(env, pattern, d)) {
exact_matches.emplace_back(*it, d.get_name());
} else {