Exporting the SearchAbout filter.

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

2 files changed, 17 insertions, 13 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
index 23cff9931..3a8faaa8d 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -23,6 +23,10 @@ open Nametab
 type filter_function = global_reference -> env -> constr -> bool
 type display_function = global_reference -> env -> constr -> unit
 
+type glob_search_about_item =
+  | GlobSearchSubPattern of constr_pattern
+  | GlobSearchString of string
+
 module SearchBlacklist =
   Goptions.MakeStringTable
     (struct
@@ -135,6 +139,15 @@ let module_filter (mods, outside) ref env typ =
   if outside then List.for_all is_outside mods
   else List.is_empty mods || List.exists is_inside mods
 
+let name_of_reference ref = Id.to_string (basename_of_global ref)
+
+let search_about_filter query gr env typ = match query with
+| GlobSearchSubPattern pat ->
+  Matching.is_matching_appsubterm ~closed:false pat typ
+| GlobSearchString s ->
+  String.string_contains ~where:(name_of_reference gr) ~what:s
+
+
 (** SearchPattern *)
 
 let search_pattern pat mods =
@@ -187,24 +200,12 @@ let search_by_head = search_pattern
 
 (** SearchAbout *)
 
-let name_of_reference ref = Id.to_string (basename_of_global ref)
-
-type glob_search_about_item =
-  | GlobSearchSubPattern of constr_pattern
-  | GlobSearchString of string
-
-let search_about_item (itemref,typ) = function
-  | GlobSearchSubPattern pat ->
-    Matching.is_matching_appsubterm ~closed:false pat typ
-  | GlobSearchString s ->
-    String.string_contains ~where:(name_of_reference itemref) ~what:s
-
 let search_about items mods =
   let ans = ref [] in
   let filter ref env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
     let f_module = module_filter mods ref env typ in
-    let f_about (b, i) = eqb b (search_about_item (ref, typ) i) in
+    let f_about (b, i) = eqb b (search_about_filter i ref env typ) in
     let f_blacklist = blacklist_filter ref env typ in
     f_module && List.for_all f_about items && f_blacklist
   in
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 301f89acb..c139c71cd 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -31,6 +31,9 @@ val blacklist_filter : filter_function
 val module_filter : DirPath.t list * bool -> filter_function
 (** Check whether a reference pertains or not to a set of modules *)
 
+val search_about_filter : glob_search_about_item -> filter_function
+(** Check whether a reference matches a SearchAbout query. *)
+
 (** {6 Specialized search functions} *)
 
 val search_by_head : constr_pattern -> DirPath.t list * bool -> std_ppcmds