From 2019b56bf43237167cc55512bbc13d82138abdb9 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 9 Sep 2012 22:24:34 +0000
Subject: When asked for a SearchAbout request, Coq now returns a more precise
 name, that is, a pair of a smart qualified name and the missing prefix needed
 to recover the full path.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15787 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/wg_ScriptView.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'ide/wg_ScriptView.ml')

diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 2c524ab74..82dd77344 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -61,7 +61,12 @@ let get_completion (buffer : GText.buffer) coqtop w =
     let query handle = match Coq.search handle flags with
     | Interface.Good l ->
       let fold accu elt =
-        Proposals.add elt.Interface.search_answer_base_name accu
+        let rec last accu = function
+        | [] -> accu
+        | [basename] -> Proposals.add basename accu
+        | _ :: l -> last accu l
+        in
+        last accu elt.Interface.coq_object_qualid
       in
       ans := (List.fold_left fold accu l)
     | _ -> ()
-- 
cgit v1.2.3