diff options
| author | ppedrot | 2012-09-09 22:24:34 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-09 22:24:34 +0000 |
| commit | 2019b56bf43237167cc55512bbc13d82138abdb9 (patch) | |
| tree | 7f35d5154b47f39d87fcdc4f2faa87a1e03280bc /ide | |
| parent | 56dc4da6ddafe885f6be0dcb300a6449541eab35 (diff) | |
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
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 7 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 7 |
3 files changed, 10 insertions, 6 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index c19fe7889a..43a040822f 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 27eb5fceab..c75a7885eb 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 2c524ab74f..82dd77344b 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) | _ -> () |