diff options
| author | slrnsc | 2021-02-02 15:17:32 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-02 15:17:32 +0000 |
| commit | f6a695c81f7833683e846dddce5d5156254eaa92 (patch) | |
| tree | 39cfb514bee6ef30b37c684844cf50d88e47f53a | |
| parent | 36b07c2194466ed79977d0195cd6567dd2059d3b (diff) | |
ide: lablgtk fixes
| -rw-r--r-- | ide/coqide/wg_Find.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml index e2f9256ef9..7f30cc8c6c 100644 --- a/ide/coqide/wg_Find.ml +++ b/ide/coqide/wg_Find.ml @@ -221,15 +221,12 @@ class finder name (view : GText.view) = (* Keypress interaction *) 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 + 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 = esc then (esc_cb (); true) + else if ev_key = GdkKeysyms._Escape then (esc_cb (); true) else false in let find_cb = dispatch_key_cb self#hide self#find_forward self#find_backward in |