Moved code out of ide_slave in a more appropriate place.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15570 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 79 insertions, 75 deletions

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 8b8de43ee1..2b5d4b5a5d 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -247,81 +247,7 @@ let status () =
     Interface.status_proofnum = Pfedit.current_proof_depth ();
   }
 
-(** This should be elsewhere... *)
-let search flags =
-  let env = Global.env () in
-  let rec extract_flags name tpe subtpe mods blacklist = function
-  | [] -> (name, tpe, subtpe, mods, blacklist)
-  | (Interface.Name_Pattern s, b) :: l ->
-    let regexp =
-      try Str.regexp s
-      with _ -> Errors.error ("Invalid regexp: " ^ s)
-    in
-    extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
-  | (Interface.Type_Pattern s, b) :: l ->
-    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
-    extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
-  | (Interface.SubType_Pattern s, b) :: l ->
-    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
-    extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
-  | (Interface.In_Module m, b) :: l ->
-    let path = String.concat "." m in
-    let m = Pcoq.parse_string Pcoq.Constr.global path in
-    let (_, qid) = Libnames.qualid_of_reference m in
-    let id =
-      try Nametab.full_name_module qid
-      with Not_found ->
-        Errors.error ("Module " ^ path ^ " not found.")
-    in
-    extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
-  | (Interface.Include_Blacklist, b) :: l ->
-    extract_flags name tpe subtpe mods b l
-  in
-  let (name, tpe, subtpe, mods, blacklist) =
-    extract_flags [] [] [] [] false flags
-  in
-  let filter_function ref env constr =
-    let id = Names.string_of_id (Nametab.basename_of_global ref) in
-    let path = Libnames.dirpath (Nametab.path_of_global ref) in
-    let toggle x b = if x then b else not b in
-    let match_name (regexp, flag) =
-      toggle (Str.string_match regexp id 0) flag
-    in
-    let match_type (pat, flag) =
-      toggle (Matching.is_matching pat constr) flag
-    in
-    let match_subtype (pat, flag) =
-      toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag
-    in
-    let match_module (mdl, flag) =
-      toggle (Libnames.is_dirpath_prefix_of mdl path) flag
-    in
-    let in_blacklist =
-      blacklist || (Search.filter_blacklist ref env constr)
-    in
-    List.for_all match_name name &&
-    List.for_all match_type tpe &&
-    List.for_all match_subtype subtpe &&
-    List.for_all match_module mods && in_blacklist
-  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))
-    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);
-    } in
-    ans := answer :: !ans;
-  in
-  let () = Search.gen_filtered_search filter_function print_function in
-  !ans
+let search flags = Search.interface_search flags
 
 let get_options () =
   let table = Goptions.get_tables () in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 520b74ada7..2e1ed1c359 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -259,3 +259,78 @@ let search_about reference inout =
   let ans = ref [] in
   raw_search_about (filter_by_module_from_list inout) (plain_display ans) reference;
   format_display !ans
+
+let interface_search flags =
+  let env = Global.env () in
+  let rec extract_flags name tpe subtpe mods blacklist = function
+  | [] -> (name, tpe, subtpe, mods, blacklist)
+  | (Interface.Name_Pattern s, b) :: l ->
+    let regexp =
+      try Str.regexp s
+      with _ -> Errors.error ("Invalid regexp: " ^ s)
+    in
+    extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
+  | (Interface.Type_Pattern s, b) :: l ->
+    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
+  | (Interface.SubType_Pattern s, b) :: l ->
+    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
+  | (Interface.In_Module m, b) :: l ->
+    let path = String.concat "." m in
+    let m = Pcoq.parse_string Pcoq.Constr.global path in
+    let (_, qid) = Libnames.qualid_of_reference m in
+    let id =
+      try Nametab.full_name_module qid
+      with Not_found ->
+        Errors.error ("Module " ^ path ^ " not found.")
+    in
+    extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
+  | (Interface.Include_Blacklist, b) :: l ->
+    extract_flags name tpe subtpe mods b l
+  in
+  let (name, tpe, subtpe, mods, blacklist) =
+    extract_flags [] [] [] [] false flags
+  in
+  let filter_function ref env constr =
+    let id = Names.string_of_id (Nametab.basename_of_global ref) in
+    let path = Libnames.dirpath (Nametab.path_of_global ref) in
+    let toggle x b = if x then b else not b in
+    let match_name (regexp, flag) =
+      toggle (Str.string_match regexp id 0) flag
+    in
+    let match_type (pat, flag) =
+      toggle (Matching.is_matching pat constr) flag
+    in
+    let match_subtype (pat, flag) =
+      toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag
+    in
+    let match_module (mdl, flag) =
+      toggle (Libnames.is_dirpath_prefix_of mdl path) flag
+    in
+    let in_blacklist =
+      blacklist || (filter_blacklist ref env constr)
+    in
+    List.for_all match_name name &&
+    List.for_all match_type tpe &&
+    List.for_all match_subtype subtpe &&
+    List.for_all match_module mods && in_blacklist
+  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))
+    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);
+    } in
+    ans := answer :: !ans;
+  in
+  let () = gen_filtered_search filter_function print_function in
+  !ans
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 343dcf76c6..3788acd05a 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -29,6 +29,9 @@ val search_pattern : constr -> dir_path list * bool -> std_ppcmds
 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
+
 (** The filtering function that is by standard search facilities.
    It can be passed as argument to the raw search functions. *)