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

feat(frontends/lean/server): take current namespace into account when processing FINDP command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-05 00:40:34 -07:00
parent 28f025c6d7
commit 5fa1c0a5fb
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "library/type_util.h"
#include "library/unifier.h"
#include "library/opaque_hints.h"
#include "library/scoped_ext.h"
#include "library/tactic/goal.h"
#include "frontends/lean/server.h"
#include "frontends/lean/parser.h"
@ -537,9 +538,21 @@ void server::find_prefix(unsigned line_num, std::string const & prefix) {
}
}
});
list<name> const & ns_list = get_namespaces(env);
env.for_each_declaration([&](declaration const & d) {
if (!already_added.contains(d.get_name()) && is_findp_prefix_of(p, d.get_name()))
display_decl(d.get_name(), d.get_name(), env, opts);
if (!already_added.contains(d.get_name()) && is_findp_prefix_of(p, d.get_name())) {
bool found = false;
name n = d.get_name();
for (name const & ns : ns_list) {
if (is_prefix_of(ns, n)) {
display_decl(n.replace_prefix(ns, name()), n, env, opts);
found = true;
break;
}
}
if (!found)
display_decl(n, n, env, opts);
}
});
m_out << "-- ENDFINDP" << std::endl;
}