From e5d61707d9baf8a4b2fa0fb1c9c5c2a1415c5f31 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 23 Oct 2006 11:40:53 +0000
Subject: fixed non-bug #1213

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9262 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 13 ++++++++++---
 1 file 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,9 +2504,13 @@ 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" 
-- 
cgit v1.2.3