From 5ee09a9ed5d0ce7508ce63b77e04879995beb33f Mon Sep 17 00:00:00 2001
From: slrnsc
Date: Mon, 1 Feb 2021 01:00:23 +0000
Subject: ide: shift+enter to find backwards

---
 ide/coqide/wg_Find.ml | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'ide')

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
 
-- 
cgit v1.2.3