diff options
| author | puech | 2010-03-11 15:02:37 +0000 |
|---|---|---|
| committer | puech | 2010-03-11 15:02:37 +0000 |
| commit | 1e936ed5151dd2b2716b8b17662e87122d92304d (patch) | |
| tree | ffefc8016f23a6a41fb50c040e929c0b53444bdb | |
| parent | d674e583e666a0a2e840163712a4e961ccac219a (diff) | |
Filter out "_subproof" objects from search results
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12857 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/search.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml index 8f31134c7c..075c80c9a2 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -168,6 +168,8 @@ let raw_search_rewrite extra_filter display_function pattern = let raw_search_by_head extra_filter display_function pattern = Util.todo "raw_search_by_head" +let name_of_reference ref = string_of_id (basename_of_global ref) + (* * functions to use the new Libtypes facility *) @@ -194,14 +196,19 @@ let filter_by_module_from_list = function | [], _ -> (fun _ _ _ -> true) | l, outside -> filter_by_module l (not outside) +let filter_subproof gr _ _ = + not (string_string_contains (name_of_reference gr) "_subproof") + +let (&&&&&) f g x y z = f x y z && g x y z + let search_by_head pat inout = - text_search_by_head (filter_by_module_from_list inout) pat + text_search_by_head (filter_by_module_from_list inout &&&&& filter_subproof) pat let search_rewrite pat inout = - text_search_rewrite (filter_by_module_from_list inout) pat + text_search_rewrite (filter_by_module_from_list inout &&&&& filter_subproof) pat let search_pattern pat inout = - text_pattern_search (filter_by_module_from_list inout) pat + text_pattern_search (filter_by_module_from_list inout &&&&& filter_subproof) pat let gen_filtered_search filter_function display_function = gen_crible None @@ -209,8 +216,6 @@ let gen_filtered_search filter_function display_function = (** SearchAbout *) -let name_of_reference ref = string_of_id (basename_of_global ref) - type glob_search_about_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string @@ -223,7 +228,7 @@ let raw_search_about filter_modules display_function l = let filter ref' env typ = filter_modules ref' env typ && List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && - not (string_string_contains (name_of_reference ref') "_subproof") + filter_subproof ref' () () in gen_filtered_search filter display_function |