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

3 files changed, 30 insertions, 26 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index 07d82352b2..f8a382aefa 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -86,10 +86,14 @@ type search_constraint =
     the flag should be negated. *)
 type search_flags = (search_constraint * bool) list
 
-type search_answer = {
-  search_answer_full_path : string list;
-  search_answer_base_name : string;
-  search_answer_type : string;
+(** A named object in Coq. [coq_object_qualid] is the shortest path defined for 
+    the user. [coq_object_prefix] is the missing part to recover the fully 
+    qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
+    [coq_object_object] is the actual content of the object. *)
+type 'a coq_object = {
+  coq_object_prefix : string list;
+  coq_object_qualid : string list;
+  coq_object_object : 'a;
 }
 
 type coq_info = {
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 2aed906b89..0f19badf49 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -47,7 +47,7 @@ type handler = {
   evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
-  search : search_flags -> search_answer list;
+  search : search_flags -> string coq_object list;
   get_options : unit -> (option_name * option_state) list;
   set_options : (option_name * option_value) list -> unit;
   inloadpath : string -> bool;
@@ -65,12 +65,12 @@ let goals : goals option call = Goal
 let evars : evar list option call = Evars
 let hints : (hint list * hint) option call = Hints
 let status : status call = Status
-let search flags : search_answer list call = Search flags
+let search flags : string coq_object list call = Search flags
 let get_options : (option_name * option_state) list call = GetOptions
 let set_options l : unit call = SetOptions l
 let inloadpath s : bool call = InLoadPath s
 let mkcases s : string list list call = MkCases s
-let search flags : search_answer list call = Search flags
+let search flags : string coq_object list call = Search flags
 let quit : unit call = Quit
 
 (** * Coq answers to CoqIde *)
@@ -91,7 +91,7 @@ let abstract_eval_call handler c =
             | Evars -> Obj.magic (handler.evars () : evar list option)
             | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
             | Status -> Obj.magic (handler.status () : status)
-            | Search flags -> Obj.magic (handler.search flags : search_answer list)
+            | Search flags -> Obj.magic (handler.search flags : string coq_object list)
             | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
             | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
             | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
@@ -242,20 +242,20 @@ let to_search_constraint xml = do_match xml "search_constraint"
   | "include_blacklist" -> Include_Blacklist
   | _ -> raise Marshal_error)
 
-let of_search_answer ans =
-  let path = of_list of_string ans.search_answer_full_path in
-  let name = of_string ans.search_answer_base_name in
-  let tpe = of_string ans.search_answer_type in
-  Element ("search_answer", [], [path; name; tpe])
-
-let to_search_answer = function
-| Element ("search_answer", [], [path; name; tpe]) ->
-  let path = to_list to_string path in
-  let name = to_string name in
-  let tpe = to_string tpe in {
-    search_answer_full_path = path;
-    search_answer_base_name = name;
-    search_answer_type = tpe;
+let of_coq_object f ans =
+  let prefix = of_list of_string ans.coq_object_prefix in
+  let qualid = of_list of_string ans.coq_object_qualid in
+  let obj = f ans.coq_object_object in
+  Element ("coq_object", [], [prefix; qualid; obj])
+
+let to_coq_object f = function
+| Element ("coq_object", [], [prefix; qualid; obj]) ->
+  let prefix = to_list to_string prefix in
+  let qualid = to_list to_string qualid in
+  let obj = f obj in {
+    coq_object_prefix = prefix;
+    coq_object_qualid = qualid;
+    coq_object_object = obj;
   }
 | _ -> raise Marshal_error
 
@@ -466,7 +466,7 @@ let of_answer (q : 'a call) (r : 'a value) =
   | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml)
   | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml)
   | Status -> Obj.magic (of_status : status -> xml)
-  | Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml)
+  | Search _ -> Obj.magic (of_list (of_coq_object of_string) : string coq_object list -> xml)
   | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml)
   | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], []))
   | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
@@ -493,7 +493,7 @@ let to_answer xml =
     | "option_value" -> Obj.magic (to_option_value elt : option_value)
     | "option_state" -> Obj.magic (to_option_state elt : option_state)
     | "coq_info" -> Obj.magic (to_coq_info elt : coq_info)
-    | "search_answer" -> Obj.magic (to_search_answer elt : search_answer)
+    | "coq_object" -> Obj.magic (to_coq_object convert elt : 'a coq_object)
     | _ -> raise Marshal_error
     end
   | _ -> raise Marshal_error
diff --git a/lib/serialize.mli b/lib/serialize.mli
index a46d3c6cc8..ad9a9c2994 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -59,7 +59,7 @@ val mkcases : string -> string list list call
 val evars : evar list option call
 
 (** Search for objects satisfying the given search flags. *)
-val search : search_flags -> search_answer list call
+val search : search_flags -> string coq_object list call
 
 (** Retrieve the list of options of the current toplevel, together with their 
     state. *)
@@ -83,7 +83,7 @@ type handler = {
   evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
-  search : search_flags -> search_answer list;
+  search : search_flags -> string coq_object list;
   get_options : unit -> (option_name * option_state) list;
   set_options : (option_name * option_value) list -> unit;
   inloadpath : string -> bool;