Renaming SearchAbout into Search and Search into SearchHead.

I hope I did not forget any place to change.

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

4 files changed, 7 insertions, 6 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 26dbcb125..ae39a1249 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -207,7 +207,8 @@ let state_preserving = [
   "Recursive Extraction Library";
 
   "Search";
-  "SearchAbout";
+  "SearchAbout (* deprecated *)";
+  "SearchHead";
   "SearchPattern";
   "SearchRewrite";
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8429a9b07..616358789 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -626,7 +626,7 @@ let otherquery command _ =
     Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
 
 let query command _ =
-  if command = "SearchAbout"
+  if command = "Search" || command = "SearchAbout"
   then searchabout ()
   else otherquery command ()
 
@@ -1054,7 +1054,7 @@ let build_ui () =
   let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in
   menu queries_menu [
     item "Queries" ~label:"_Queries";
-    qitem "SearchAbout" (Some "F2");
+    qitem "Search" (Some "F2");
     qitem "Check" (Some "F3");
     qitem "Print" (Some "F4");
     qitem "About" (Some "F5");
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index d88f623ef..8732cd83b 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -110,7 +110,7 @@ let init () =
     %s
   </menu>
   <menu action='Queries'>
-    <menuitem action='SearchAbout' />
+    <menuitem action='Search' />
     <menuitem action='Check' />
     <menuitem action='Print' />
     <menuitem action='About' />
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index e21cc0aa0..319342e91 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -253,10 +253,10 @@ class finder (view : GText.view) =
 class info (coqtop : Coq.coqtop) (view : GText.view) (msg_view : Wg_MessageView.message_view) =
 
   let widget = GPack.vbox () in
-  (* SearchAbout part *)
+  (* Search part *)
   let query_box = GPack.hbox ~packing:widget#add () in
   let _ =
-    GMisc.label ~text:"SearchAbout:"
+    GMisc.label ~text:"Search:"
       ~xalign:1.0
       ~packing:query_box#pack ()
   in