diff options
| -rw-r--r-- | doc/changelog/09-coqide/13810-shift-return-search-backwards.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 2 | ||||
| -rw-r--r-- | ide/coqide/wg_Find.ml | 16 |
3 files changed, 13 insertions, 8 deletions
diff --git a/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst new file mode 100644 index 0000000000..e78280d91d --- /dev/null +++ b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst @@ -0,0 +1,3 @@ +- **Added:** + Shift-return in the Find dialog now searches backwards (`#13810 <https://github.com/coq/coq/pull/13810>`_, + by slrnsc). diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 93d70c773f..4ea9606c18 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -880,7 +880,7 @@ started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-opt .. _qualified-names: Qualified identifiers ---------------------- +~~~~~~~~~~~~~~~~~~~~~ .. insertprodn qualid field_ident diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml index 7e89191bd1..7f30cc8c6c 100644 --- a/ide/coqide/wg_Find.ml +++ b/ide/coqide/wg_Find.ml @@ -219,16 +219,18 @@ 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 (return, _) = GtkData.AccelGroup.parse "Return" in - let (esc, _) = GtkData.AccelGroup.parse "Escape" in - if ev_key = return then (ret_cb (); true) - else if ev_key = esc then (esc_cb (); true) + let ev_modifiers = GdkEvent.Key.state ev in + if ev_key = GdkKeysyms._Return then + (if List.mem `SHIFT ev_modifiers then + shift_ret_cb () + else ret_cb (); true) + else if ev_key = GdkKeysyms._Escape 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 |