diff options
| -rw-r--r-- | INSTALL.ide | 9 | ||||
| -rw-r--r-- | ide/FAQ | 7 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 318 | ||||
| -rw-r--r-- | ide/coqide.ml | 36 | ||||
| -rw-r--r-- | ide/preferences.ml | 7 |
5 files changed, 202 insertions, 175 deletions
diff --git a/INSTALL.ide b/INSTALL.ide index 4d2b123d8..f3a0c868c 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -64,14 +64,17 @@ INSTALLATION make install-ide NOTES -There are two configuration files located in your $(HOME) dir. You may need to - set HOME to any sensible value under Windows. +There are three configuration files located in your $(HOME) dir. + You may need to set HOME to some sensible value under Windows. - .coqiderc is generated by coqide itself. It may be edited by hand or using the Preference menu from coqide. It will be generated the first time you save your preferences in Coqide. - .coqide-gtk2rc is a standard Gtk2 configuration file. A sample file can be - found in the coq lib ide subdir. + found in the coq lib "ide" subdir. + +- .coqide.keys is a standard Gtk2 accelerator dump. You may edit this file + to change the default shortcuts for the menus. Read ide/FAQ for more informations. @@ -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 |