From 26192480f1f23b9854f36a242dc4476ac823c0ba Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 13 Feb 2013 17:35:23 +0000 Subject: CoqIDE: Adding escape reaction to replace widget git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16202 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/wg_Find.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'ide/wg_Find.ml') diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index b810bf78a..2746975cc 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -219,15 +219,19 @@ class finder (view : GText.view) = let _ = r_previous_button#connect#clicked ~callback:self#find_backward in let _ = r_replace_button#connect#clicked ~callback:self#replace in let _ = r_replace_all_button#connect#clicked ~callback:self#replace_all in - let find_cb ev = + let generic_cb esc_cb ret_cb ev = let ev_key = GdkEvent.Key.keyval ev in 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) + if ev_key = return then (ret_cb (); true) + else if ev_key = esc then (esc_cb (); true) else false in + let find_cb = generic_cb self#hide self#find_forward in + let replace_cb = generic_cb self#hide self#replace in let _ = find_entry#event#connect#key_press find_cb in + let _ = r_find_entry#event#connect#key_press replace_cb in + let _ = r_replace_entry#event#connect#key_press find_cb in () end -- cgit v1.2.3