Error messages of Searchxxx are coherent with goal selector.

If a goal is given and wrong, exception is raised. If no goal is
given, then goal 1 is tried but no failure if goal 1 does not exist,
just fall back to gloab env.

3 files changed, 35 insertions, 31 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
index 8336b488a..26e6416a9 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -53,13 +53,11 @@ let iter_named_context_name_type f = List.iter (fun (nme,_,typ) -> f nme typ)
 
 (* General search over hypothesis of a goal *)
 let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
-  try
-    let env = Global.env () in
-    let iter_hyp idh typ = fn (VarRef idh) env typ in
-    let evmap,e = Pfedit.get_goal_context glnum in
-    let pfctxt = named_context e in
-    iter_named_context_name_type iter_hyp pfctxt
-  with _ -> ()
+  let env = Global.env () in
+  let iter_hyp idh typ = fn (VarRef idh) env typ in
+  let evmap,e = Pfedit.get_goal_context glnum in
+  let pfctxt = named_context e in
+  iter_named_context_name_type iter_hyp pfctxt
 
 (* General search over declarations *)
 let iter_declarations (fn : global_reference -> env -> constr -> unit) =
@@ -93,8 +91,10 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   try Declaremods.iter_all_segments iter_obj
   with Not_found -> ()
 
-let generic_search glnum fn =
-  iter_hypothesis glnum fn;
+let generic_search glnumopt fn =
+  (match glnumopt with
+  | None -> ()
+  | Some glnum ->  iter_hypothesis glnum fn);
   iter_declarations fn
 
 (** Standard display *)
@@ -156,7 +156,7 @@ let search_about_filter query gr env typ = match query with
 
 (** SearchPattern *)
 
-let search_pattern g pat mods =
+let search_pattern gopt pat mods =
   let ans = ref [] in
   let filter ref env typ =
     let f_module = module_filter mods ref env typ in
@@ -167,7 +167,7 @@ let search_pattern g pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search g iter in
+  let () = generic_search gopt iter in
   format_display !ans
 
 (** SearchRewrite *)
@@ -180,7 +180,7 @@ let rewrite_pat1 pat =
 let rewrite_pat2 pat =
   PApp (PRef eq, [| PMeta None; PMeta None; pat |])
 
-let search_rewrite g pat mods =
+let search_rewrite gopt pat mods =
   let pat1 = rewrite_pat1 pat in
   let pat2 = rewrite_pat2 pat in
   let ans = ref [] in
@@ -196,12 +196,12 @@ let search_rewrite g pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search g iter in
+  let () = generic_search gopt iter in
   format_display !ans
 
 (** Search *)
 
-let search_by_head g pat mods =
+let search_by_head gopt pat mods =
   let ans = ref [] in
   let filter ref env typ =
     let f_module = module_filter mods ref env typ in
@@ -212,12 +212,12 @@ let search_by_head g pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search g iter in
+  let () = generic_search gopt iter in
   format_display !ans
 
 (** SearchAbout *)
 
-let search_about g items mods =
+let search_about gopt items mods =
   let ans = ref [] in
   let filter ref env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
@@ -229,7 +229,7 @@ let search_about g items mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search g iter in
+  let () = generic_search gopt iter in
   format_display !ans
 
 type search_constraint =
@@ -333,5 +333,5 @@ let interface_search flags =
   let iter ref env typ =
     if filter_function ref env typ then print_function ref env typ
   in
-  let () = generic_search 1 iter in (* TODO: chose a goal number? *)
+  let () = generic_search None iter in (* TODO: chose a goal number? *)
   !ans
diff --git a/toplevel/search.mli b/toplevel/search.mli
index f5d1d13ed..2d1d9622d 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -39,10 +39,10 @@ val search_about_filter : glob_search_about_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_rewrite : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_pattern : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_about   : int -> (bool * glob_search_about_item) list
+val search_by_head : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_pattern : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_about   : int option -> (bool * glob_search_about_item) list
   -> DirPath.t list * bool -> std_ppcmds
 
 type search_constraint =
@@ -68,6 +68,6 @@ val interface_search : (search_constraint * bool) list ->
 
 (** {6 Generic search function} *)
 
-val generic_search : int -> display_function -> unit
+val generic_search : int option -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e3b94a777..287bf2304 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1645,21 +1645,25 @@ let interp_search_about_item env =
           	as an identifier component")
 
 let vernac_search s gopt r =
-  let g = Option.default 1 gopt in
   let r = interp_search_restriction r in
-  let env =
-    try snd (Pfedit.get_goal_context g)
-    with _ -> Global.env () in
+  let env,gopt =
+    match gopt with | None ->
+      (* 1st goal by default if it exists, otherwise no goal at all *)
+      (try snd (Pfedit.get_goal_context 1) , Some 1
+       with _ -> Global.env (),None)
+    (* if goal selector is given and wrong, then let exceptions be raised. *)
+    | Some g -> snd (Pfedit.get_goal_context g) , Some g
+  in
   let get_pattern c = snd (intern_constr_pattern env c) in
   match s with
   | SearchPattern c ->
-      msg_notice (Search.search_pattern g (get_pattern c) r)
+      msg_notice (Search.search_pattern gopt (get_pattern c) r)
   | SearchRewrite c ->
-      msg_notice (Search.search_rewrite g (get_pattern c) r)
+      msg_notice (Search.search_rewrite gopt (get_pattern c) r)
   | SearchHead c ->
-      msg_notice (Search.search_by_head g (get_pattern c) r)
+      msg_notice (Search.search_by_head gopt (get_pattern c) r)
   | SearchAbout sl ->
-     msg_notice (Search.search_about g (List.map (on_snd (interp_search_about_item env)) sl) r)
+     msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r)
 
 let vernac_locate = function
   | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)