CoqIde: AccelMap support

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4001 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 196 insertions, 172 deletions

diff --git a/ide/FAQ b/ide/FAQ
index ba97211e5..53b34d7ea 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -54,4 +54,9 @@ R6) Use
     or 
 	coqmktop -ide -opt m1.cmx...mi.cmx
 
-
+Q7) How to customize the shortcuts for menus?
+R6) Two solutions are offered:
+  - Edit $HOME/.coqide.keys by hand
+  - Add "gtk-can-change-accels = 1" in your .coqiderc.gtk2 file. Then
+    from CoqIde, you may select a menu entry and press the desired 
+    shortcut. Do not forget to save your preferences.
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 9cd851820..9598ee2f6 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -10,184 +10,184 @@
 
 let commands = [
   ["Abort";
-  "Add Abstract Ring";
-  "Add Abstract Semi Ring";
-  "Add Field";
-  "Add LoadPath";
-  "Add ML Path";
-  "Add Morphism";
-  "Add Printing If";
-  "Add Printing Let";
-  "Add Rec LoadPath";
-  "Add Rec ML Path";
-  "Add Ring";
-  "Add Semi Ring";
-  "Add Semi Ring";
-  "Add Setoid";
-  "Axiom";];
+   "Add Abstract Ring";
+   "Add Abstract Semi Ring";
+   "Add Field";
+   "Add LoadPath";
+   "Add ML Path";
+   "Add Morphism";
+   "Add Printing If";
+   "Add Printing Let";
+   "Add Rec LoadPath";
+   "Add Rec ML Path";
+   "Add Ring";
+   "Add Semi Ring";
+   "Add Semi Ring";
+   "Add Setoid";
+   "Axiom";];
   ["Back";
-  "Begin Silent";];
+   "Begin Silent";];
   ["Canonical Structure";
-  "Cd";
-  "Chapter";
-  "Check";
-  "Coercion";
-  "Coercion Local";
-  "CoFixpoint";
-  "CoInductive";
-  "Correctness";];
+   "Cd";
+   "Chapter";
+   "Check";
+   "Coercion";
+   "Coercion Local";
+   "CoFixpoint";
+   "CoInductive";
+   "Correctness";];
   ["Declare ML Module";
-  "Defined";
-  "Definition";
-  "Derive Dependent Inversion";
-  "Derive Dependent Inversion_clear";
-  "Derive Inversion";
-  "Derive Inversion_clear";
-  "Drop";];
+   "Defined";
+   "Definition";
+   "Derive Dependent Inversion";
+   "Derive Dependent Inversion_clear";
+   "Derive Inversion";
+   "Derive Inversion_clear";
+   "Drop";];
   ["End";
-  "End Silent";
-  "Eval";
-  "Explicitation of implicit arguments";
-  "Extract Constant";
-  "Extract Inductive";
-  "Extraction";
-  "Extraction Inline";
-  "Extraction Language";
-  "Extraction Module";
-  "Extraction NoInline";];
+   "End Silent";
+   "Eval";
+   "Explicitation of implicit arguments";
+   "Extract Constant";
+   "Extract Inductive";
+   "Extraction";
+   "Extraction Inline";
+   "Extraction Language";
+   "Extraction Module";
+   "Extraction NoInline";];
   ["Fact";
-  "Fixpoint";
-  "Focus";];
+   "Fixpoint";
+   "Focus";];
   ["Global Variable";
-  "Goal";
-  "Grammar";];
+   "Goal";
+   "Grammar";];
   ["Hint";
    "Hint Constructors";
-  "Hint Unfold";
-  "Hint";
-  "Hint Rewrite";
-  "Hints Extern";
-  "Hints Immediate";
-  "Hints Resolve";
-  "Hints Immediate";
-  "Hints Resolve";
-  "Hints Unfold";
-  "Hypothesis";];
+   "Hint Unfold";
+   "Hint";
+   "Hint Rewrite";
+   "Hints Extern";
+   "Hints Immediate";
+   "Hints Resolve";
+   "Hints Immediate";
+   "Hints Resolve";
+   "Hints Unfold";
+   "Hypothesis";];
   ["Identity Coercion";
-  "Implicit Arguments Off";
-  "Implicit Arguments On";
-  "Implicits";
-  "Inductive";
-  "Infix";
-  "Inspect";];
+   "Implicit Arguments Off";
+   "Implicit Arguments On";
+   "Implicits";
+   "Inductive";
+   "Infix";
+   "Inspect";];
   ["Lemma";
-  "Load";
-  "Load Verbose";
-  "Local";
-  "Locate";
-  "Locate File";
-  "Locate Library";];
+   "Load";
+   "Load Verbose";
+   "Local";
+   "Locate";
+   "Locate File";
+   "Locate Library";];
   ["Module";
-  "Module Type";
-  "Mutual Inductive";];
+   "Module Type";
+   "Mutual Inductive";];
   ["Notation";];
   ["Opaque";];
   ["Parameter";
-  "Print";
-  "Print All";
-  "Print Classes";
-  "Print Coercion Paths";
-  "Print Coercions";
-  "Print Extraction Inline";
-  "Print Graph";
-  "Print Hint";
-  "Print HintDb";
-  "Print LoadPath";
-  "Print ML Modules";
-  "Print ML Path";
-  "Print Module";
-  "Print Module Type";
-  "Print Modules";
-  "Print Proof";
-  "Print Section";
-  "Print Table Printing If";
-  "Print Table Printing Let";
-  "Proof";
-  "Pwd";];
+   "Print";
+   "Print All";
+   "Print Classes";
+   "Print Coercion Paths";
+   "Print Coercions";
+   "Print Extraction Inline";
+   "Print Graph";
+   "Print Hint";
+   "Print HintDb";
+   "Print LoadPath";
+   "Print ML Modules";
+   "Print ML Path";
+   "Print Module";
+   "Print Module Type";
+   "Print Modules";
+   "Print Proof";
+   "Print Section";
+   "Print Table Printing If";
+   "Print Table Printing Let";
+   "Proof";
+   "Pwd";];
   ["Qed";
-  "Quit";];
+   "Quit";];
   ["Read Module";
-  "Record";
-  "Recursive Extraction";
-  "Recursive Extraction Module";
-  "Remark";
-  "Remove LoadPath";
-  "Remove Printing If";
-  "Remove Printing Let";
-  "Require";
-  "Require Export";
-  "Reset";
-  "Reset Extraction Inline";
-  "Reset Initial";
-  "Restart";
-  "Restore State";
-  "Resume";];
-[  "Save";
-  "Scheme";
-  "Search";
-  "Search ... inside ...";
-  "Search ... outside ...";
-  "SearchAbout";
-  "SearchPattern";
-  "SearchPattern ... inside ...";
-  "SearchPattern ... outside ...";
-  "SearchRewrite";
-  "SearchRewrite ... inside ...";
-  "SearchRewrite ... outside ...";
-  "Section";
-  "Set Extraction AutoInline";
-  "Set Extraction Optimize";
-  "Set Hyps_limit";
-  "Set Implicit Arguments";
-  "Set Printing Coercion";
-  "Set Printing Coercions";
-  "Set Printing Synth";
-  "Set Printing Wildcard";
-  "Set Undo";
-  "Show";
-  "Show Conjectures";
-  "Show Implicits";
-  "Show Intro";
-  "Show Intros";
-  "Show Programs";
-  "Show Proof";
-  "Show Script";
-  "Show Tree";
-  "Structure";
-  "Suspend";
-  "Syntactic Definition";
-  "Syntax";];
+   "Record";
+   "Recursive Extraction";
+   "Recursive Extraction Module";
+   "Remark";
+   "Remove LoadPath";
+   "Remove Printing If";
+   "Remove Printing Let";
+   "Require";
+   "Require Export";
+   "Reset";
+   "Reset Extraction Inline";
+   "Reset Initial";
+   "Restart";
+   "Restore State";
+   "Resume";];
+  [  "Save";
+     "Scheme";
+     "Search";
+     "Search ... inside ...";
+     "Search ... outside ...";
+     "SearchAbout";
+     "SearchPattern";
+     "SearchPattern ... inside ...";
+     "SearchPattern ... outside ...";
+     "SearchRewrite";
+     "SearchRewrite ... inside ...";
+     "SearchRewrite ... outside ...";
+     "Section";
+     "Set Extraction AutoInline";
+     "Set Extraction Optimize";
+     "Set Hyps_limit";
+     "Set Implicit Arguments";
+     "Set Printing Coercion";
+     "Set Printing Coercions";
+     "Set Printing Synth";
+     "Set Printing Wildcard";
+     "Set Undo";
+     "Show";
+     "Show Conjectures";
+     "Show Implicits";
+     "Show Intro";
+     "Show Intros";
+     "Show Programs";
+     "Show Proof";
+     "Show Script";
+     "Show Tree";
+     "Structure";
+     "Suspend";
+     "Syntactic Definition";
+     "Syntax";];
   ["Tactic Definition";
-  "Test Printing If";
-  "Test Printing Let";
-  "Test Printing Synth";
-  "Test Printing Wildcard";
-  "Theorem";
-  "Time";
-  "Transparent";];
+   "Test Printing If";
+   "Test Printing Let";
+   "Test Printing Synth";
+   "Test Printing Wildcard";
+   "Theorem";
+   "Time";
+   "Transparent";];
   ["Undo";
-  "Unfocus";
-  "Unset Extraction AutoInline";
-  "Unset Extraction Optimize";
-  "Unset Hyps_limit";
-  "Unset Implicit Arguments";
-  "Unset Printing Coercion";
-  "Unset Printing Coercions";
-  "Unset Printing Synth";
-  "Unset Printing Wildcard";
-  "Unset Undo";];
+   "Unfocus";
+   "Unset Extraction AutoInline";
+   "Unset Extraction Optimize";
+   "Unset Hyps_limit";
+   "Unset Implicit Arguments";
+   "Unset Printing Coercion";
+   "Unset Printing Coercions";
+   "Unset Printing Synth";
+   "Unset Printing Wildcard";
+   "Unset Undo";];
   ["Variable";
-  "Variables";];
+   "Variables";];
   ["Write State";];
 ]
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index db87e47b9..f4f26ee57 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -31,7 +31,6 @@ let small_size = `SMALL_TOOLBAR
 
 let initial_cwd = Sys.getcwd ()
 
-
 let status = ref None
 let push_info = ref (function s -> failwith "not ready")
 let pop_info = ref (function s -> failwith "not ready")
@@ -1520,12 +1519,13 @@ let main files =
   show_toolbar := 
   (fun b -> if b then handle#misc#show () else handle#misc#hide ());
 
-  let factory = new GMenu.factory menubar in
+  let factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/" menubar in
   let accel_group = factory#accel_group in
 
   (* File Menu *)
   let file_menu = factory#add_submenu "_File" in
-  let file_factory = new GMenu.factory file_menu ~accel_group in
+
+  let file_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/File/" file_menu ~accel_group in
 
   (* File/Load Menu *)
   let load f =
@@ -1568,7 +1568,8 @@ let main files =
       | Vector.Found i -> set_current_view i
       | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
   in
-  let load_m = file_factory#add_item "_Open/Create" ~key:GdkKeysyms._O in
+  let load_m = file_factory#add_item "_Open/Create" 
+		 ~key:GdkKeysyms._O in
   let load_f () = 	  
     match  select_file ~title:"Load file" () with 
       | None -> ()
@@ -1577,7 +1578,8 @@ let main files =
   ignore (load_m#connect#activate (load_f));
 
   (* File/Save Menu *)
-  let save_m = file_factory#add_item "_Save" ~key:GdkKeysyms._S in
+  let save_m = file_factory#add_item "_Save" 
+		 ~key:GdkKeysyms._S in
   let save_f () = 
     let current = get_current_view () in
     try
@@ -1605,7 +1607,8 @@ let main files =
   ignore (save_m#connect#activate save_f);
 
   (* File/Save As Menu *)
-  let saveas_m = file_factory#add_item "S_ave as" in
+  let saveas_m = file_factory#add_item "S_ave as" 
+  in
   let saveas_f () = 
     let current = get_current_view () in
     try (match (out_some current.analyzed_view)#filename with 
@@ -1734,7 +1737,7 @@ let main files =
   in
   let file_export_m =  file_factory#add_submenu "E_xport to" in
 
-  let file_export_factory = new GMenu.factory file_export_m ~accel_group in
+  let file_export_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Export/" file_export_m ~accel_group in
   let export_html_m = 
     file_export_factory#add_item "_Html" ~callback:(export_f "html") 
   in
@@ -1779,13 +1782,14 @@ let main files =
 	| _ -> ()
     else exit 0
   in
-  let quit_m = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q ~callback:quit_f
+  let quit_m = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q 
+		 ~callback:quit_f
   in
   ignore (w#event#connect#delete (fun _ -> quit_f (); true));
 
   (* Edit Menu *)
   let edit_menu = factory#add_submenu "_Edit" in
-  let edit_f = new GMenu.factory edit_menu ~accel_group in
+  let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
   ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
 	   (do_if_not_computing 
 	      (fun () -> ignore (get_current_view()).view#undo)));
@@ -1811,8 +1815,9 @@ let main files =
 		 with _ -> prerr_endline "EMIT PASTE FAILED")));
   ignore (edit_f#add_separator ());
   let read_only_i = edit_f#add_check_item "Expert" ~active:false
-		      ~key:GdkKeysyms._Z
+		      (* ~key:GdkKeysyms._Z *)
 		      ~callback:(fun b -> 
+				   (* GtkData.AccelMap.save "test.accel" *) 
 				   ()
 				) 
   in
@@ -1845,6 +1850,7 @@ let main files =
   let navigation_menu =  factory#add_submenu "_Navigation" in
   let navigation_factory = 
     new GMenu.factory navigation_menu 
+      ~accel_path:"<CoqIde MenuBar>/Navigation/"
       ~accel_group 
       ~accel_modi:!current.modifier_for_navigation 
   in
@@ -1917,6 +1923,7 @@ let main files =
   let tactics_menu =  factory#add_submenu "_Try Tactics" in
   let tactics_factory = 
     new GMenu.factory tactics_menu 
+      ~accel_path:"<CoqIde MenuBar>/Tactics/"
       ~accel_group 
       ~accel_modi:!current.modifier_for_tactics
   in
@@ -1988,6 +1995,7 @@ let main files =
   (* Templates Menu *)
   let templates_menu =  factory#add_submenu "Te_mplates" in
   let templates_factory = new GMenu.factory templates_menu 
+			    ~accel_path:"<CoqIde MenuBar>/Templates/"
 			    ~accel_group 
 			    ~accel_modi:!current.modifier_for_templates
   in
@@ -2106,6 +2114,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   (* Commands Menu *)
   let commands_menu =  factory#add_submenu "_Commands" in
   let commands_factory = new GMenu.factory commands_menu ~accel_group
+			   ~accel_path:"<CoqIde MenuBar>/Commands"
 			   ~accel_modi:[]
   in
   
@@ -2143,7 +2152,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
   (* Externals *)
   let externals_menu =  factory#add_submenu "_Externals" in
-  let externals_factory = new GMenu.factory externals_menu ~accel_group in
+  let externals_factory = new GMenu.factory externals_menu 
+			    ~accel_path:"<CoqIde MenuBar>/Externals/"
+			    ~accel_group in
   
   (* Command/Compile Menu *)
   let compile_f () =
@@ -2215,7 +2226,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   in reset_auto_save_timer (); (* to enable statup preferences timer *)
 
   let configuration_menu = factory#add_submenu "Confi_guration" in
-  let configuration_factory = new GMenu.factory configuration_menu ~accel_group
+  let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Configuration" ~accel_group
   in
   let edit_prefs_m =
     configuration_factory#add_item "Edit _preferences"
@@ -2276,6 +2287,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
   let help_menu = factory#add_submenu "_Help" in
   let help_factory = new GMenu.factory help_menu  
+		       ~accel_path:"<CoqIde MenuBar>/Help/"
 		       ~accel_modi:[]
 		       ~accel_group in
   let _ = help_factory#add_item "Browse Coq _Manual" 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c6a1aabdd..0ee8bec55 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -16,6 +16,10 @@ let pref_file =
   try (Filename.concat (Sys.getenv "HOME") ".coqiderc")
   with _ -> ".coqiderc"
 
+let accel_file = 
+  try (Filename.concat (Sys.getenv "HOME") ".coqide.keys")
+  with _ -> ".coqide.keys"
+
 let mod_to_str (m:Gdk.Tags.modifier) = 
   match m with
     | `MOD1 -> "MOD1"
@@ -133,6 +137,8 @@ let show_toolbar = ref (fun x -> ())
 let resize_window = ref (fun () -> ())
 
 let save_pref () =
+  (try GtkData.AccelMap.save accel_file 
+  with _ -> ());
   let p = !current in
   try 
     let add = Stringmap.add in
@@ -173,6 +179,7 @@ let save_pref () =
   
 
 let load_pref () =
+  (try GtkData.AccelMap.load accel_file with _ -> ());
   let p = !current in 
   try 
     let m = Config_lexer.load_file pref_file in