aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-02 19:25:13 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-02 19:25:13 +0000
commit8211140b73a3e1132ab70d8d75d4debc6e48ea4f (patch)
treeb9ac35e4a1901a695fe2e86029b9a137f9bab98c /toplevel
parenta9ecb7e57fed81f936045f30830322834f95a17e (diff)
Exporting the SearchAbout filter.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16379 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/search.ml27
-rw-r--r--toplevel/search.mli3
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