From 41c25a6d99e4c6f3e7f95f751ec302720d7755d5 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 25 Jan 2013 23:21:28 +0000
Subject: Better handling of escape find in CoqIDE

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16148 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml             | 2 --
 ide/coqide_ui.ml          | 1 -
 ide/mac_default_accel_map | 1 -
 ide/wg_Find.ml            | 6 ++++--
 4 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7b5ccca83e..d48e7d4a5e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -931,8 +931,6 @@ let build_ui () =
       ~callback:(fun _ -> notebook#current_term.finder#find_backward ());
     item "Replace" ~stock:`FIND_AND_REPLACE
       ~callback:(fun _ -> notebook#current_term.finder#show `REPLACE);
-    item "Close Find" ~accel:"Escape"
-      ~callback:(fun _ -> notebook#current_term.finder#hide ());
     item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash"
       ~callback:(fun _ ->
         ignore ( ()
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 36e071e862..d88f623eff 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -20,7 +20,6 @@ let list_items menu li =
 
 let init () =
   let theui = Printf.sprintf "<ui>
-<accelerator action='Close Find' />
 <menubar name='CoqIde MenuBar'>
   <menu action='File'>
     <menuitem action='New' />
diff --git a/ide/mac_default_accel_map b/ide/mac_default_accel_map
index 28ff7b9a9f..6f474eb124 100644
--- a/ide/mac_default_accel_map
+++ b/ide/mac_default_accel_map
@@ -244,7 +244,6 @@
 ; (gtk_accel_path "<Actions>/Templates/Template Notation" "")
 ; (gtk_accel_path "<Actions>/Edit/Cut" "<Primary>x")
 ; (gtk_accel_path "<Actions>/Templates/Template Theorem" "")
-; (gtk_accel_path "<Actions>/Edit/Close Find" "Escape")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "")
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 7dc4adfea2..b810bf78a6 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -221,8 +221,10 @@ class finder (view : GText.view) =
       let _ = r_replace_all_button#connect#clicked ~callback:self#replace_all in
       let find_cb ev =
         let ev_key = GdkEvent.Key.keyval ev in
-        let (key, _) = GtkData.AccelGroup.parse "Return" in
-        if ev_key = key then (self#find_forward (); true)
+        let (return, _) = GtkData.AccelGroup.parse "Return" in
+        let (esc, _) = GtkData.AccelGroup.parse "Escape" in
+        if ev_key = return then (self#find_forward (); true)
+        else if ev_key = esc then (self#hide (); true)
         else false
       in
       let _ = find_entry#event#connect#key_press find_cb in
-- 
cgit v1.2.3