aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.mli2
-rw-r--r--ide/coqide.ml7
-rw-r--r--ide/wg_ScriptView.ml7
-rw-r--r--lib/interface.mli12
-rw-r--r--lib/serialize.ml40
-rw-r--r--lib/serialize.mli4
-rw-r--r--toplevel/search.ml24
-rw-r--r--toplevel/search.mli2
8 files changed, 58 insertions, 40 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index c19fe7889..43a040822 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -99,7 +99,7 @@ val evars : handle -> Interface.evar list option Interface.value
val hints : handle -> (Interface.hint list * Interface.hint) option Interface.value
val inloadpath : handle -> string -> bool Interface.value
val mkcases : handle -> string -> string list list Interface.value
-val search : handle -> Interface.search_flags -> Interface.search_answer list Interface.value
+val search : handle -> Interface.search_flags -> string Interface.coq_object list Interface.value
(** A specialized version of [raw_interp] dedicated to
set/unset options. *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 27eb5fcea..c75a7885e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1744,10 +1744,9 @@ let main files =
let results = match results with | Interface.Good l -> l | _ -> [] in
let buf = term.message_view#buffer in
let insert result =
- let basename = result.Interface.search_answer_base_name in
- let path = result.Interface.search_answer_full_path in
- let name = String.concat "." path ^ "." ^ basename in
- let tpe = result.Interface.search_answer_type in
+ let qualid = result.Interface.coq_object_qualid in
+ let name = String.concat "." qualid in
+ let tpe = result.Interface.coq_object_object in
buf#insert ~tags:[Tags.Message.item] name;
buf#insert "\n";
buf#insert tpe;
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)
| _ -> ()
diff --git a/lib/interface.mli b/lib/interface.mli
index 07d82352b..f8a382aef 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 2aed906b8..0f19badf4 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 a46d3c6cc..ad9a9c299 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;
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 9d6be8e5c..3ab4feb5e 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -320,15 +320,25 @@ let interface_search flags =
in
let ans = ref [] in
let print_function ref env constr =
- let name = Names.string_of_id (Nametab.basename_of_global ref) in
- let make_path = Names.string_of_id in
- let path =
- List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref))
+ let fullpath = repr_dirpath (Nametab.dirpath_of_global ref) in
+ let qualid = Nametab.shortest_qualid_of_global Idset.empty ref in
+ let (shortpath, basename) = Libnames.repr_qualid qualid in
+ let shortpath = repr_dirpath shortpath in
+ (* [shortpath] is a suffix of [fullpath] and we're looking for the missing
+ prefix *)
+ let rec prefix full short accu = match full, short with
+ | _, [] ->
+ let full = List.rev_map string_of_id full in
+ (full, accu)
+ | _ :: full, m :: short ->
+ prefix full short (string_of_id m :: accu)
+ | _ -> assert false
in
+ let (prefix, qualid) = prefix fullpath shortpath [string_of_id basename] in
let answer = {
- Interface.search_answer_full_path = path;
- Interface.search_answer_base_name = name;
- Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr);
+ Interface.coq_object_prefix = prefix;
+ Interface.coq_object_qualid = qualid;
+ Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr);
} in
ans := answer :: !ans;
in
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 6dfc87596..56b6a1bda 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -30,7 +30,7 @@ val search_about :
(bool * glob_search_about_item) list -> dir_path list * bool -> std_ppcmds
val interface_search : (Interface.search_constraint * bool) list ->
- Interface.search_answer list
+ string Interface.coq_object list
(** The filtering function that is by standard search facilities.
It can be passed as argument to the raw search functions. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 17:37:13 +0000