diff options
| author | ppedrot | 2012-05-02 17:00:59 +0000 |
|---|---|---|
| committer | ppedrot | 2012-05-02 17:00:59 +0000 |
| commit | 7b1a9e289de1bd792f49ad6ab0ded0b2fdebb972 (patch) | |
| tree | 23989e5ff2ed1f45335116cf41593688aa836813 | |
| parent | c64fe271b2ad1bb748257f84f0de438755593966 (diff) | |
Fixed #2769
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15264 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/coqide.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index b0afbc1073..dae237660b 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1185,13 +1185,18 @@ object(self) ("progress "^p^".\n") (p^".\n")) l) method private active_keypress_handler k = -(* let state = GdkEvent.Key.state k in *) begin if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin - prerr_endline "active_kp_handler for Tab"; - self#indent_current_line; - true + let state = GdkEvent.Key.state k in + let is_control = List.mem `CONTROL state in + if is_control then + begin + prerr_endline "active_kp_handler for Tab"; + self#indent_current_line; + true + end + else false end else false @@ -2206,9 +2211,9 @@ let main files = (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ]; GAction.add_actions view_actions [ GAction.add_action "View" ~label:"_View"; - GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<SHIFT>Left") ~stock:`GO_BACK + GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<Ctrl><Shift>Tab") ~stock:`GO_BACK ~callback:(fun _ -> session_notebook#previous_page ()); - GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<SHIFT>Right") ~stock:`GO_FORWARD + GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<Ctrl>Tab") ~stock:`GO_FORWARD ~callback:(fun _ -> session_notebook#next_page ()); GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar" ~active:(!current.show_toolbar) ~callback: |