diff options
| author | barras | 2006-10-23 11:40:53 +0000 |
|---|---|---|
| committer | barras | 2006-10-23 11:40:53 +0000 |
| commit | e5d61707d9baf8a4b2fa0fb1c9c5c2a1415c5f31 (patch) | |
| tree | bd708afef49ce5855acbae644e947346301a0ee9 | |
| parent | a7cce63afed99a666cb893430bdc81ed0a6c67c3 (diff) | |
fixed non-bug #1213
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9262 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/coqide.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 343096f5b4..908c1b7986 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2017,7 +2017,8 @@ let main files = ignore (revert_m#connect#activate revert_f); (* File/Close Menu *) - let close_m = file_factory#add_item "_Close Buffer" in + let close_m = + file_factory#add_item "_Close Buffer" ~key:GdkKeysyms._W in let close_f () = let v = out_some !active_view in let act = get_current_view_page () in @@ -2042,7 +2043,9 @@ let main files = let s,_ = run_command av#insert_message cmd in !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in - let _ = file_factory#add_item "_Print" ~callback:print_f in + let _ = file_factory#add_item "_Print" + ~key:GdkKeysyms._P + ~callback:print_f in (* File/Export to Menu *) let export_f kind () = @@ -2501,10 +2504,14 @@ let main files = add_to_menu_toolbar "_Save" ~tooltip:"Save current buffer" - (* ~key:GdkKeysyms._Down *) ~callback:save_f `SAVE; add_to_menu_toolbar + "_Close" + ~tooltip:"Close current buffer" + ~callback:close_f + `CLOSE; + add_to_menu_toolbar "_Forward" ~tooltip:"Forward one command" ~key:GdkKeysyms._Down |