ide: shift+enter to find backwards

1 files changed, 9 insertions, 4 deletions

diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml
index 7e89191bd1..e2f9256ef9 100644
--- a/ide/coqide/wg_Find.ml
+++ b/ide/coqide/wg_Find.ml
@@ -219,16 +219,21 @@ class finder name (view : GText.view) =
       let _ = replace_all_button#connect#clicked ~callback:self#replace_all in
 
       (* Keypress interaction *)
-      let generic_cb esc_cb ret_cb ev =
+      let dispatch_key_cb esc_cb ret_cb shift_ret_cb ev =
         let ev_key = GdkEvent.Key.keyval ev in
+        let ev_state = GdkEvent.Key.state ev in
+        let ev_modifiers = Gdk.Convert.modifier ev_state in
         let (return, _) = GtkData.AccelGroup.parse "Return" in
         let (esc, _) = GtkData.AccelGroup.parse "Escape" in
-        if ev_key = return then (ret_cb (); true)
+        if ev_key = return then
+          (if List.mem `SHIFT ev_modifiers then
+            shift_ret_cb ()
+          else 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_cb = dispatch_key_cb self#hide self#find_forward self#find_backward in
+      let replace_cb = dispatch_key_cb self#hide self#replace self#replace in
       let _ = find_entry#event#connect#key_press ~callback:find_cb in
       let _ = replace_entry#event#connect#key_press ~callback:replace_cb in