From 5fa1c0a5fb5ea7a8ac9421285f1957bc90ce8b57 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Sep 2014 00:40:34 -0700 Subject: [PATCH] feat(frontends/lean/server): take current namespace into account when processing FINDP command Signed-off-by: Leonardo de Moura --- src/frontends/lean/server.cpp | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 52711bfcc..447768881 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -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 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; }