Integration de SearchNamed dans SearchAbout

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

7 files changed, 57 insertions, 18 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index a7bd150532..4290eca610 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -550,12 +550,16 @@ let solve_hook n =
 
 let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 
+let interp_search_about_item = function
+  | SearchRef qid -> SearchRef (Nametab.global qid)
+  | SearchString s as x -> x
+
 let pcoq_search s l =
   ctv_SEARCH_LIST:=[];
   begin match s with
-  | SearchAbout locqid -> 
+  | SearchAbout sl -> 
       raw_search_about (filter_by_module_from_list l) add_search
-	(Nametab.global locqid)
+	(List.map interp_search_about_item sl)
   | SearchPattern c ->
       let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
       raw_pattern_search (filter_by_module_from_list l) add_search pat
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index fad041f209..67078ab237 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -102,8 +102,12 @@ GEXTEND Gram
 	  VernacSearch (SearchPattern c, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
-      | IDENT "SearchAbout"; qid = global; l = in_or_out_modules -> 
-	  VernacSearch (SearchAbout qid, l)
+      | IDENT "SearchAbout"; 
+	  sl = [ "["; l = LIST1 [ r = global -> Search.SearchRef r
+                                  | s = STRING -> Search.SearchString s ]; "]" -> l 
+   		 | qid = global -> [Search.SearchRef qid] ];
+	  l = in_or_out_modules -> 
+	  VernacSearch (SearchAbout sl, l)
       | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> 
 	  VernacSearch (SearchNamed sl, l)
 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 9e718cfd65..93baa3edfb 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -519,8 +519,12 @@ GEXTEND Gram
 	  VernacSearch (SearchPattern c, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
-      | IDENT "SearchAbout"; qid = global; l = in_or_out_modules -> 
-	  VernacSearch (SearchAbout qid, l)
+      | IDENT "SearchAbout"; 
+	  sl = [ "["; l = LIST1 [ r = global -> Search.SearchRef r
+                                  | s = STRING -> Search.SearchString s ]; "]" -> l 
+   		 | qid = global -> [Search.SearchRef qid] ];
+	  l = in_or_out_modules -> 
+	  VernacSearch (SearchAbout sl, l)
       | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> 
 	  VernacSearch (SearchNamed sl, l)
 
diff --git a/parsing/search.ml b/parsing/search.ml
index 4413376cbe..336398e2bd 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -94,6 +94,7 @@ let rec head c =
   let c = strip_outer_cast c in
   match kind_of_term c with
   | Prod (_,_,c) -> head c
+  | LetIn (_,_,_,c) -> head c
   | _              -> c
       
 let constr_to_section_path c = match kind_of_term c with
@@ -200,24 +201,39 @@ let gen_filtered_search filter_function display_function =
   gen_crible None
     (fun s a c -> if filter_function s a c then display_function s a c) 
 
-let raw_search_about filter_modules display_function ref =
-  let c = constr_of_reference ref in
+(** SearchAbout *)
+
+let name_of_reference ref = string_of_id (id_of_global ref)
+
+type 'a search_about_item =
+  | SearchRef of 'a
+  | SearchString of string
+
+let search_about_item (itemref,typ) = function
+  | SearchRef ref -> Termops.occur_term (constr_of_reference ref) typ
+  | SearchString s -> string_string_contains (name_of_reference itemref) s
+
+let raw_search_about filter_modules display_function l =
   let filter ref' env typ =
     filter_modules ref' env typ &&
-    Termops.occur_term c typ
+    List.for_all (search_about_item (ref',typ)) l
   in
   gen_filtered_search filter display_function
 
 let search_about ref inout = 
   raw_search_about (filter_by_module_from_list inout) plain_display ref
 
-let name_of_reference ref = string_of_id (id_of_global ref)
+(** SearchNamed *)
+
+let close_string s = 
+  if s.[String.length s - 1] = '*' then String.sub s 0 (String.length s - 1)
+  else s^"_"
 
 let occur_string_in_name name s =
   let l = String.length s + 1 in
   let l' = String.length name in
-  string_string_contains name ("_"^s^"_")
-  || l' >= l && String.sub name 0 l = (s^"_")
+  string_string_contains name (close_string ("_"^s))
+  || l' >= l && String.sub name 0 l = (close_string s)
   || l' >= l && String.sub name (l'-l) l = ("_"^s)
 
 let raw_search_named filter_modules display_function strings =
@@ -230,4 +246,3 @@ let raw_search_named filter_modules display_function strings =
 
 let search_named strings inout =
   raw_search_named (filter_by_module_from_list inout) plain_display strings
-
diff --git a/parsing/search.mli b/parsing/search.mli
index d53c3fecf3..260c12e9d6 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -18,10 +18,15 @@ open Nametab
 
 (*s Search facilities. *)
 
+type 'a search_about_item =
+  | SearchRef of 'a
+  | SearchString of string
+
 val search_by_head : global_reference -> dir_path list * bool -> unit
 val search_rewrite : constr_pattern -> dir_path list * bool -> unit
 val search_pattern : constr_pattern -> dir_path list * bool -> unit
-val search_about   : global_reference -> dir_path list * bool -> unit
+val search_about   : global_reference search_about_item list ->
+      dir_path list * bool -> unit
 val search_named   : string list -> dir_path list * bool -> unit
 
 (* The filtering function that is by standard search facilities.
@@ -40,6 +45,7 @@ val raw_pattern_search : (global_reference -> env -> constr -> bool) ->
 val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
   (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
 val raw_search_about : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> global_reference -> unit
+  (global_reference -> env -> constr -> unit) -> 
+      global_reference search_about_item list -> unit
 val raw_search_named : (global_reference -> env -> constr -> bool) ->
   (global_reference -> env -> constr -> unit) -> string list -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9c248e9dc4..a0137d7911 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -880,6 +880,12 @@ let interp_search_restriction = function
   | SearchOutside l -> (List.map global_module l, true)
   | SearchInside l -> (List.map global_module l, false)
 
+open Search
+
+let interp_search_about_item = function
+  | SearchRef qid -> SearchRef (Nametab.global qid)
+  | SearchString s as x -> x
+
 let vernac_search s r =
   let r = interp_search_restriction r in
   if !pcoq <> None then (out_some !pcoq).search s r else
@@ -892,8 +898,8 @@ let vernac_search s r =
       Search.search_rewrite pat r
   | SearchHead locqid ->
       Search.search_by_head (Nametab.global locqid) r
-  | SearchAbout locqid ->
-      Search.search_about (Nametab.global locqid) r
+  | SearchAbout sl ->
+      Search.search_about (List.map interp_search_about_item sl) r
   | SearchNamed strings ->
       Search.search_named strings r
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 61d468fe5a..76c3358a02 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -59,7 +59,7 @@ type searchable =
   | SearchPattern of pattern_expr
   | SearchRewrite of pattern_expr
   | SearchHead of reference
-  | SearchAbout of reference
+  | SearchAbout of reference Search.search_about_item list
   | SearchNamed of string list
 
 type locatable =