diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-25 23:21:28 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-25 23:21:28 +0000 |
| commit | 41c25a6d99e4c6f3e7f95f751ec302720d7755d5 (patch) | |
| tree | 10e98c69bc9c6ee00cedacf1831795bd79510fcb /ide | |
| parent | 8f0c821091a20ad652690154ce865c0e784218de (diff) | |
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
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 1 | ||||
| -rw-r--r-- | ide/mac_default_accel_map | 1 | ||||
| -rw-r--r-- | ide/wg_Find.ml | 6 |
4 files changed, 4 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 7b5ccca83..d48e7d4a5 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 36e071e86..d88f623ef 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 28ff7b9a9..6f474eb12 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 7dc4adfea..b810bf78a 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 |