From 9b24b6d763bb2c7975cd2b93364d7647fd660598 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Apr 2013 18:33:16 +0000
Subject: 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
---
 ide/coq_commands.ml | 3 ++-
 ide/coqide.ml       | 4 ++--
 ide/coqide_ui.ml    | 2 +-
 ide/wg_Find.ml      | 4 ++--
 4 files changed, 7 insertions(+), 6 deletions(-)

(limited to 'ide')

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 26dbcb125b..ae39a1249d 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 8429a9b07a..6163587899 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 d88f623eff..8732cd83b4 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 e21cc0aa05..319342e919 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
-- 
cgit v1.2.3