diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-10 18:35:06 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-10 18:35:06 +0000 |
commit | 6858036c6d12d77df2da9643b04f56733428be13 (patch) | |
tree | 6e2c0986dc71b88229084c9b112666d93b73a1c5 | |
parent | 8de2295f3becd3aa7116c0710122efd63144b0ce (diff) |
Coqide Menubar integration in MacOS
Because of lablgtk issues, accel_maps can't be customized well on MacOS
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile.build | 5 | ||||
-rw-r--r-- | config/Makefile.template | 2 | ||||
-rwxr-xr-x | configure | 8 | ||||
-rw-r--r-- | ide/coqide.ml | 7 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 8 | ||||
-rw-r--r-- | ide/coqide_ui.ml | 3 | ||||
-rw-r--r-- | ide/ide_mac_stubs.c | 42 | ||||
-rw-r--r-- | ide/mac_default_accel_map | 372 | ||||
-rw-r--r-- | ide/preferences.ml | 3 |
9 files changed, 431 insertions, 19 deletions
diff --git a/Makefile.build b/Makefile.build index 587be3bd7..852ce0042 100644 --- a/Makefile.build +++ b/Makefile.build @@ -329,7 +329,7 @@ install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info install-ide-no: -install-ide-byte: +install-ide-byte: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ @@ -346,6 +346,7 @@ install-ide-opt: install-ide-files: $(MKDIR) $(FULLIDELIB) $(INSTALLLIB) $(IDEFILES) $(FULLIDELIB) + if [ $(IDEOPTINT) = "MacInt" ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(INSTALLLIB)/ide/default_accel_map ; fi install-ide-info: $(MKDIR) $(FULLIDELIB) @@ -707,7 +708,7 @@ ide/coqide_main.ml: ide/coqide_main.ml4 ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4USE) $(IDEOPTP4) -impl $< -o $@ + $(HIDE)$(CAMLP4O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@ # pretty printing of the revision number when compiling a checked out diff --git a/config/Makefile.template b/config/Makefile.template index c5d81c9d0..e9067e98f 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -140,7 +140,7 @@ STRIP=STRIPCOMMAND HASCOQIDE=COQIDEOPT IDEOPTFLAGS=IDEARCHFLAGS IDEOPTDEPS=IDEARCHFILE -IDEOPTP4=IDEARCHDEF +IDEOPTINT=IDEARCHDEF # Defining REVISION CHECKEDOUT=CHECKEDOUTSOURCETREE @@ -599,7 +599,7 @@ esac IDEARCHFLAGS= IDEARCHFILE= -IDEARCHDEF= +IDEARCHDEF=No # -byte-only should imply -coqide byte, unless the user decides otherwise @@ -647,12 +647,12 @@ else cflags=$cflags" `pkg-config --cflags ige-mac-integration`" IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"' IDEARCHFILE=ide/ide_mac_stubs.o - IDEARCHDEF=-DMacInt + IDEARCHDEF=MacInt elif [ "$ARCH" = "win32" ]; then IDEARCHFLAGS= IDEARCHFILE=ide/ide_win32_stubs.o - IDEARCHDEF=-DWin32 + IDEARCHDEF=Win32 fi fi fi @@ -881,7 +881,7 @@ fi if test "$COQIDE" != "no"; then echo " Lablgtk2 library in : $LABLGTKLIB" fi -if test "$IDEARCHDEF" = "-DMacInt"; then +if test "$IDEARCHDEF" = "MacInt"; then echo " Mac OS integration is on" fi if test "$with_doc" = "all"; then diff --git a/ide/coqide.ml b/ide/coqide.ml index b0fadaca2..a57551b80 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2537,7 +2537,8 @@ let main files = Coqide_ui.ui_m#insert_action_group windows_actions 0; Coqide_ui.ui_m#insert_action_group help_actions 0; w#add_accel_group Coqide_ui.ui_m#get_accel_group ; - vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar"); + if Gdk.Windowing.platform <> `QUARTZ + then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar"); let tbar = GtkButton.Toolbar.cast ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget) in let () = GtkButton.Toolbar.set ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar in @@ -2811,9 +2812,7 @@ let main files = end; initial_about session_notebook#current_term.proof_view#buffer; !show_toolbar !current.show_toolbar; - session_notebook#current_term.script#misc#grab_focus () - -;; + session_notebook#current_term.script#misc#grab_focus ();; (* This function check every half of second if GeoProof has send something on his private clipboard *) diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 9a9a0a0ed..0f9964814 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -10,13 +10,14 @@ IFDEF MacInt THEN external gtk_mac_init : (string -> unit) -> (unit -> bool) -> unit = "caml_gtk_mac_init" -external gtk_mac_ready : unit -> unit +external gtk_mac_ready : ([> Gtk.widget ] as 'a) Gtk.obj -> ([> Gtk.widget ] as 'a) Gtk.obj -> + ([> Gtk.widget ] as 'a) Gtk.obj -> unit = "caml_gtk_mac_ready" END let initmac () = IFDEF MacInt THEN gtk_mac_init Coqide.do_load Coqide.forbid_quit_to_save ELSE () END -let macready () = IFDEF MacInt THEN gtk_mac_ready () ELSE () END +let macready x y z = IFDEF MacInt THEN gtk_mac_ready x#as_widget y#as_widget z#as_widget ELSE () END (* On win32, we add the directory of coqide to the PATH at launch-time (this used to be done in a .bat script). *) @@ -89,7 +90,8 @@ let () = else failwith ("Coqide internal error: " ^ msg))); Coqide.main files; if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ()); - macready () ; + macready (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs") + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help/Abt"); while true do try GtkThread.main () diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 0ea018fc4..d3543cf2c 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -38,7 +38,7 @@ let init () = <menuitem action='Ps' /> </menu> <menuitem action='Rehighlight' /> - <menuitem action='Quit' /> + %s </menu> <menu name='Edit' action='Edit'> <menuitem action='Undo' /> @@ -144,6 +144,7 @@ let init () = <toolitem action='Wizard' /> </toolbar> </ui>" + (if Gdk.Windowing.platform <> `QUARTZ then "<menuitem action='Quit' />" else "") (Buffer.contents (list_items "Tactic" Coq_commands.tactics)) (Buffer.contents (list_items "Template" Coq_commands.commands)) in diff --git a/ide/ide_mac_stubs.c b/ide/ide_mac_stubs.c index 87cdbf08a..64deb71d0 100644 --- a/ide/ide_mac_stubs.c +++ b/ide/ide_mac_stubs.c @@ -4,10 +4,33 @@ #include <caml/callback.h> #include <caml/fail.h> +#include <gtk/gtk.h> +#include <lablgtk2/wrappers.h> +#include <lablgtk2/ml_glib.h> +#include <lablgtk2/ml_gobject.h> #include <igemacintegration/gtkosxapplication.h> GtkOSXApplication *theApp; -value open_file_fun, forbid_quit_fun; +value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item; + +static void osx_accel_map_foreach_lcb(gpointer data,const gchar *accel_path, + guint accel_key, GdkModifierType accel_mods, + gboolean changed) { + if (accel_mods & GDK_CONTROL_MASK) { + accel_mods |= GDK_META_MASK; + accel_mods &= (accel_mods & GDK_MOD1_MASK) ? ~GDK_MOD1_MASK : ~GDK_CONTROL_MASK; + if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) { + g_print("could not change accelerator %s\n",accel_path); + } + } + if (accel_mods & GDK_MOD1_MASK) { + accel_mods &= ~ GDK_MOD1_MASK; + accel_mods |= GDK_CONTROL_MASK; + if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) { + g_print("could not change accelerator %s\n",accel_path); + } + } +} static gboolean deal_with_open(GtkOSXApplication *app, gchar *path, gpointer user_data) { @@ -41,9 +64,22 @@ CAMLprim value caml_gtk_mac_init(value open_file_the_fun, value forbid_quit_the_ CAMLreturn (Val_unit); } -CAMLprim value caml_gtk_mac_ready(value unit) +CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about) { - CAMLparam1(unit); + GtkOSXApplicationMenuGroup * pref_grp, * about_grp; + CAMLparam3(menubar,prefs,about); + themenubar = menubar; + pref_item = prefs; + about_item = about; + caml_register_generational_global_root(&themenubar); + caml_register_generational_global_root(&pref_item); + caml_register_generational_global_root(&about_item); + /* gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/ + gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar)); + about_grp = gtk_osxapplication_add_app_menu_group(theApp); + pref_grp = gtk_osxapplication_add_app_menu_group(theApp); + gtk_osxapplication_add_app_menu_item(theApp,about_grp,check_cast(GTK_MENU_ITEM,about_item)); + gtk_osxapplication_add_app_menu_item(theApp,pref_grp,check_cast(GTK_MENU_ITEM,pref_item)); gtk_osxapplication_ready(theApp); CAMLreturn(Val_unit); } diff --git a/ide/mac_default_accel_map b/ide/mac_default_accel_map new file mode 100644 index 000000000..4d34636f4 --- /dev/null +++ b/ide/mac_default_accel_map @@ -0,0 +1,372 @@ +; coqide.opt GtkAccelMap rc-file -*- scheme -*- +; this file is an automated accelerator map dump +; +; (gtk_accel_path "<DEFAULT ROOT>/C_anonical Structure/" "") +; (gtk_accel_path "<DEFAULT ROOT>/M_odule Type/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ompute/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_E.../" "") +(gtk_accel_path "<Actions>/Templates/match" "<Shift><Meta>c") +; (gtk_accel_path "<DEFAULT ROOT>/D_erive Inversion/" "") +; (gtk_accel_path "<Actions>/Queries/Check" "F3") +; (gtk_accel_path "<DEFAULT ROOT>/i_dtac/" "") +; (gtk_accel_path "<DEFAULT ROOT>/L_oad/" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_ssert/" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_irstorder using/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_olve/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_l.../" "") +(gtk_accel_path "<Actions>/Templates/Inductive" "<Shift><Meta>i") +; (gtk_accel_path "<DEFAULT ROOT>/a_ssert (__:__)/" "") +; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing Synth/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_R.../" "") +; (gtk_accel_path "<Actions>/Help/Browse Coq Library" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nset Extraction Optimize/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_imple inversion/" "") +(gtk_accel_path "<Actions>/Edit/Copy" "<Meta>c") +; (gtk_accel_path "<DEFAULT ROOT>/E_xtract Inductive/" "") +(gtk_accel_path "<Actions>/Edit/Cut" "<Meta>x") +; (gtk_accel_path "<DEFAULT ROOT>/i_nfo/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_emove Printing If/" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_apply/" "") +; (gtk_accel_path "<DEFAULT ROOT>/F_ixpoint/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_hange __ in/" "") +; (gtk_accel_path "<DEFAULT ROOT>/l_apply/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_imple induction/" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_ail/" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_lim/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite <- __ in/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Printing Let/" "") +; (gtk_accel_path "<DEFAULT ROOT>/T_ransparent/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_d.../" "") +(gtk_accel_path "<Actions>/Tactics/Wizard" "<Meta><Control>dollar") +; (gtk_accel_path "<Actions>/Windows/Detach View" "") +; (gtk_accel_path "<DEFAULT ROOT>/T_heorem/" "") +(gtk_accel_path "<Actions>/Templates/Scheme" "<Shift><Meta>s") +; (gtk_accel_path "<DEFAULT ROOT>/R_emark/" "") +; (gtk_accel_path "<Actions>/Compile/Compile" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Relation/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_ename __ into/" "") +; (gtk_accel_path "<Actions>/File/Save as" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_irstorder/" "") +; (gtk_accel_path "<DEFAULT ROOT>/G_rammar/" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_irstorder with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_ed/" "") +; (gtk_accel_path "<DEFAULT ROOT>/D_efinition/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_equire Import/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_iscriminate/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_ntro after/" "") +; (gtk_accel_path "<Actions>/Export/Latex" "") +; (gtk_accel_path "<DEFAULT ROOT>/j_p/" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_uto with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_ection/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite/" "") +; (gtk_accel_path "<Actions>/Export/Html" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_i.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_utorewrite/" "") +; (gtk_accel_path "<DEFAULT ROOT>/F_ocus/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_O.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/l_azy in/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion__clear __ with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_utrewrite/" "") +(gtk_accel_path "<Actions>/Edit/Undo" "<Meta>u") +; (gtk_accel_path "<DEFAULT ROOT>/c_onstructor __ with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_ing/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ependent rewrite <-/" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_limtype/" "") +(gtk_accel_path "<Actions>/Tactics/simpl" "<Meta><Control>s") +; (gtk_accel_path "<DEFAULT ROOT>/H_int/" "") +; (gtk_accel_path "<DEFAULT ROOT>/H_int Rewrite/" "") +; (gtk_accel_path "<DEFAULT ROOT>/V_ariable/" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nset Implicit Arguments/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_implify__eq/" "") +; (gtk_accel_path "<Actions>/Compile/Next error" "F7") +; (gtk_accel_path "<Actions>/Edit/Edit" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_et Extraction Optimize/" "") +; (gtk_accel_path "<DEFAULT ROOT>/H_ypothesis/" "") +; (gtk_accel_path "<DEFAULT ROOT>/E_nd Silent./" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_yntax/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ecide equality/" "") +; (gtk_accel_path "<DEFAULT ROOT>/O_paque/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_T.../" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_a.../" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_G.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ase/" "") +(gtk_accel_path "<Actions>/Navigation/Backward" "<Meta><Control>Up") +; (gtk_accel_path "<DEFAULT ROOT>/C_oFixpoint/" "") +; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Fixpoint/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion__clear/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ase __ with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_ssumption/" "") +; (gtk_accel_path "<DEFAULT ROOT>/t_ransitivity/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_ntros until/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_plit/" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_xists/" "") +(gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Meta>t") +; (gtk_accel_path "<Actions>/Navigation/Navigation" "") +; (gtk_accel_path "<DEFAULT ROOT>/H_int Unfold/" "") +; (gtk_accel_path "<DEFAULT ROOT>/I_mplicit Arguments/" "") +; (gtk_accel_path "<Actions>/Help/Help" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ecompose sum/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "") +; (gtk_accel_path "<CoqIde MenuBar>/Te_mplates/" "") +(gtk_accel_path "<Actions>/Edit/Find in buffer" "<Meta>f") +; (gtk_accel_path "<DEFAULT ROOT>/r_eplace __ with/" "") +(gtk_accel_path "<Actions>/Tactics/omega" "<Meta><Control>o") +; (gtk_accel_path "<DEFAULT ROOT>/S_cheme/" "") +; (gtk_accel_path "<DEFAULT ROOT>/L_emma/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nversion__clear __ in/" "") +; (gtk_accel_path "<DEFAULT ROOT>/E_xtraction Inline/" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_yntactic Definition/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nstantiate (__:=__)/" "") +; (gtk_accel_path "<DEFAULT ROOT>/C_hapter/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_L.../" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_f.../" "") +; (gtk_accel_path "<Actions>/Queries/Queries" "") +; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing Wildcard/" "") +(gtk_accel_path "<Actions>/File/Open" "<Meta>o") +; (gtk_accel_path "<DEFAULT ROOT>/f_old __ in/" "") +(gtk_accel_path "<Actions>/Navigation/Go to" "<Meta><Control>Right") +; (gtk_accel_path "<Actions>/Export/Export to" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ongruence/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_learbody/" "") +(gtk_accel_path "<Actions>/File/Close buffer" "<Meta>w") +; (gtk_accel_path "<DEFAULT ROOT>/a_pply/" "") +; (gtk_accel_path "<Actions>/Queries/SearchAbout" "F2") +; (gtk_accel_path "<DEFAULT ROOT>/i_ntro/" "") +; (gtk_accel_path "<DEFAULT ROOT>/H_int Immediate/" "") +; (gtk_accel_path "<DEFAULT ROOT>/p_ose __:=__)/" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nset Undo/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_s.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Definition/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_equire/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ompare/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_ymmetry in/" "") +(gtk_accel_path "<Actions>/Display/Display coercions" "<Shift><Control>c") +(gtk_accel_path "<Actions>/Navigation/Previous" "<Meta><Control>less") +(gtk_accel_path "<Actions>/Display/Display all low-level contents" "<Shift><Control>l") +; (gtk_accel_path "<DEFAULT ROOT>/C_oercion Local/" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_ix __ with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd ML Path/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_xiom/" "") +; (gtk_accel_path "<Actions>/Templates/Templates" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_bstract/" "") +; (gtk_accel_path "<Actions>/Edit/Clear Undo Stack" "") +(gtk_accel_path "<Actions>/File/New" "<Meta>n") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_hnf/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_o/" "") +; (gtk_accel_path "<DEFAULT ROOT>/E_xtract Constant/" "") +; (gtk_accel_path "<DEFAULT ROOT>/E_nd/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_Qed./" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Rec ML Path/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_D.../" "") +(gtk_accel_path "<Actions>/Navigation/Hide" "<Meta><Control>h") +; (gtk_accel_path "<DEFAULT ROOT>/c_ofix/" "") +; (gtk_accel_path "<CoqIde MenuBar>/_Try Tactics/" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_et Printing Wildcard/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nversion__clear/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_V.../" "") +; (gtk_accel_path "<Actions>/Export/Ps" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nset Hyps__limit/" "") +; (gtk_accel_path "<DEFAULT ROOT>/H_int Extern/" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_unctional induction/" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nset Extraction AutoInline/" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nfocus/" "") +; (gtk_accel_path "<Actions>/Edit/External editor" "") +; (gtk_accel_path "<DEFAULT ROOT>/I_dentity Coercion/" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_bsurd/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_hange/" "") +(gtk_accel_path "<Actions>/Tactics/eauto" "<Meta><Control>e") +; (gtk_accel_path "<DEFAULT ROOT>/O_bligations Tactic/" "") +(gtk_accel_path "<Actions>/Tactics/trivial" "<Meta><Control>v") +; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_bv/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. /" "") +; (gtk_accel_path "<DEFAULT ROOT>/p_ose/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_et (__:=__)/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_equire Export/" "") +; (gtk_accel_path "<DEFAULT ROOT>/L_tac/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Rec LoadPath/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_c.../" "") +(gtk_accel_path "<Actions>/Navigation/End" "<Meta><Control>End") +(gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Meta>l") +(gtk_accel_path "<Actions>/Navigation/Start" "<Meta><Control>Home") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_I.../" "") +(gtk_accel_path "<Actions>/File/Print..." "<Meta>p") +; (gtk_accel_path "<DEFAULT ROOT>/d_ependent rewrite ->/" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_tructure/" "") +; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing Let/" "") +; (gtk_accel_path "<DEFAULT ROOT>/T_ime/" "") +; (gtk_accel_path "<DEFAULT ROOT>/g_eneralize/" "") +(gtk_accel_path "<Actions>/Display/Display all basic low-level contents" "<Shift><Control>a") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_p.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_old/" "") +; (gtk_accel_path "<DEFAULT ROOT>/H_int Resolve/" "") +; (gtk_accel_path "<DEFAULT ROOT>/M_utual Inductive/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nversion __ in/" "") +; (gtk_accel_path "<Actions>/Windows/Show/Hide Toolbar" "") +(gtk_accel_path "<Actions>/File/Save" "<Meta>s") +; (gtk_accel_path "<Actions>/File/Save all" "") +; (gtk_accel_path "<Actions>/Queries/Print" "F4") +; (gtk_accel_path "<DEFAULT ROOT>/c_onstructor/" "") +; (gtk_accel_path "<Actions>/Export/Dvi" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_etoid__replace/" "") +; (gtk_accel_path "<DEFAULT ROOT>/D_efined./" "") +; (gtk_accel_path "<DEFAULT ROOT>/I_nfix/" "") +(gtk_accel_path "<Actions>/Navigation/Next" "<Meta><Control>greater") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Morphism/" "") +; (gtk_accel_path "<Actions>/Windows/Windows" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_xact/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_bv in/" "") +; (gtk_accel_path "<DEFAULT ROOT>/t_ry/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_A.../" "") +(gtk_accel_path "<Actions>/Display/Display notations" "<Shift><Control>n") +; (gtk_accel_path "<DEFAULT ROOT>/c_lear/" "") +; (gtk_accel_path "<Actions>/Compile/Make" "F6") +(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Meta><Control>ampersand") +; (gtk_accel_path "<Actions>/Help/Browse Coq Manual" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_N.../" "") +(gtk_accel_path "<Actions>/File/Quit" "<Meta>q") +; (gtk_accel_path "<DEFAULT ROOT>/u_nfold/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_u.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ouble induction/" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_et Silent./" "") +; (gtk_accel_path "<DEFAULT ROOT>/V_ariables/" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nset Printing Wildcard/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite <-/" "") +; (gtk_accel_path "<DEFAULT ROOT>/I_nductive/" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_auto with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_epeat/" "") +; (gtk_accel_path "<Actions>/Queries/Locate" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_et Hyps__limit/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Abstract Semi Ring A Aplus Amult Aone Azero Aeq T./" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ompute in/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_F.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/G_lobal Variable/" "") +; (gtk_accel_path "<DEFAULT ROOT>/t_auto/" "") +; (gtk_accel_path "<DEFAULT ROOT>/E_xtraction NoInline/" "") +; (gtk_accel_path "<DEFAULT ROOT>/u_nfold __ in/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_imple destruct/" "") +(gtk_accel_path "<Actions>/Navigation/Interrupt" "<Meta><Control>Break") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_S.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_njection/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_ead Module/" "") +; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Lemma/" "") +; (gtk_accel_path "<DEFAULT ROOT>/U_nset Silent./" "") +(gtk_accel_path "<Actions>/Display/Display universe levels" "<Shift><Control>u") +; (gtk_accel_path "<DEFAULT ROOT>/f_ourier/" "") +; (gtk_accel_path "<DEFAULT ROOT>/D_erive Inversion__clear/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_omega/" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_et Undo/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]./" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_impl __ in/" "") +; (gtk_accel_path "<Actions>/Windows/Show/Hide Query Pane" "Escape") +; (gtk_accel_path "<DEFAULT ROOT>/R_estore State/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_emove Printing Let/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Printing If/" "") +(gtk_accel_path "<Actions>/Tactics/tauto" "<Meta><Control>p") +; (gtk_accel_path "<DEFAULT ROOT>/s_impl/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_ntros/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_ymmetry/" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ut/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_efine/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_e.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_exact/" "") +(gtk_accel_path "<Actions>/Navigation/Forward" "<Meta><Control>Down") +(gtk_accel_path "<Actions>/Edit/Paste" "<Meta>v") +; (gtk_accel_path "<DEFAULT ROOT>/C_oercion/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_r.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_estruct/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Setoid/" "") +; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "") +; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing If/" "") +; (gtk_accel_path "<Actions>/Display/Display" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_move __ after/" "") +(gtk_accel_path "<Actions>/Edit/Complete Word" "<Meta>slash") +; (gtk_accel_path "<DEFAULT ROOT>/s_ubst/" "") +; (gtk_accel_path "<Actions>/Help/About Coq" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_etoid__rewrite/" "") +; (gtk_accel_path "<Actions>/Tactics/Try Tactics" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_C.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/L_ocal/" "") +; (gtk_accel_path "<DEFAULT ROOT>/s_et/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_quote/" "") +(gtk_accel_path "<Actions>/Templates/Definition" "<Shift><Meta>d") +; (gtk_accel_path "<DEFAULT ROOT>/S_et Implicit Arguments/" "") +; (gtk_accel_path "<Actions>/File/Revert all buffers" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_P.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/t_rivial/" "") +(gtk_accel_path "<Actions>/Display/Display existential variable instances" "<Shift><Control>e") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_j.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd LoadPath/" "") +; (gtk_accel_path "<DEFAULT ROOT>/N_otation/" "") +; (gtk_accel_path "<Actions>/Edit/Preferences" "") +; (gtk_accel_path "<DEFAULT ROOT>/L_oad Verbose/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_ntro __ after/" "") +; (gtk_accel_path "<DEFAULT ROOT>/D_erive Dependent Inversion/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion __ with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Theorem/" "") +; (gtk_accel_path "<DEFAULT ROOT>/E_xtraction Language/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_U.../" "") +(gtk_accel_path "<Actions>/Display/Display raw matching expressions" "<Shift><Control>m") +; (gtk_accel_path "<DEFAULT ROOT>/c_asetype/" "") +(gtk_accel_path "<Actions>/Edit/Find backwards" "<Meta>b") +; (gtk_accel_path "<DEFAULT ROOT>/S_ave./" "") +; (gtk_accel_path "<DEFAULT ROOT>/p_attern/" "") +; (gtk_accel_path "<DEFAULT ROOT>/M_odule/" "") +; (gtk_accel_path "<DEFAULT ROOT>/D_eclare ML Module/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_H.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/F_act/" "") +; (gtk_accel_path "<DEFAULT ROOT>/A_dd Field/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_emove LoadPath/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_Write State/" "") +; (gtk_accel_path "<Actions>/Compile/Make makefile" "") +; (gtk_accel_path "<DEFAULT ROOT>/C_oInductive/" "") +; (gtk_accel_path "<Actions>/Compile/Compile buffer" "") +; (gtk_accel_path "<DEFAULT ROOT>/l_eft/" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_pply __ with/" "") +(gtk_accel_path "<Actions>/File/Rehighlight" "<Meta>l") +; (gtk_accel_path "<Actions>/File/File" "") +; (gtk_accel_path "<DEFAULT ROOT>/D_erive Dependent Inversion__clear/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ecompose/" "") +; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite __ in/" "") +(gtk_accel_path "<Actions>/Display/Display implicit arguments" "<Shift><Control>i") +; (gtk_accel_path "<DEFAULT ROOT>/e_lim __ using/" "") +; (gtk_accel_path "<DEFAULT ROOT>/a_ssert (__:=__)/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nversion __ using/" "") +; (gtk_accel_path "<DEFAULT ROOT>/P_arameter/" "") +; (gtk_accel_path "<DEFAULT ROOT>/H_int Constructors/" "") +; (gtk_accel_path "<DEFAULT ROOT>/j_p <n>/" "") +; (gtk_accel_path "<DEFAULT ROOT>/p_rogress/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Templates/_M.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_lim __ with/" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_irst/" "") +; (gtk_accel_path "<DEFAULT ROOT>/l_azy/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nversion/" "") +(gtk_accel_path "<Actions>/Help/Help for keyword" "<Meta>h") +; (gtk_accel_path "<DEFAULT ROOT>/a_uto/" "") +; (gtk_accel_path "<DEFAULT ROOT>/G_oal/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nversion __ using __ in/" "") +(gtk_accel_path "<Actions>/Tactics/intuition" "<Meta><Control>i") +; (gtk_accel_path "<DEFAULT ROOT>/r_ed in/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_g.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/g_eneralize dependent/" "") +; (gtk_accel_path "<Actions>/Queries/About" "F5") +; (gtk_accel_path "<DEFAULT ROOT>/r_ight/" "") +(gtk_accel_path "<Actions>/Tactics/auto" "<Meta><Control>a") +(gtk_accel_path "<Actions>/Templates/Fixpoint" "<Shift><Meta>f") +; (gtk_accel_path "<DEFAULT ROOT>/r_eflexivity/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_nduction/" "") +; (gtk_accel_path "<DEFAULT ROOT>/i_ntuition/" "") +; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_t.../" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_ix/" "") +; (gtk_accel_path "<Actions>/Export/Pdf" "") +; (gtk_accel_path "<DEFAULT ROOT>/N_ext Obligation/" "") +(gtk_accel_path "<Actions>/Tactics/auto with *" "<Meta><Control>asterisk") +; (gtk_accel_path "<DEFAULT ROOT>/R_ecord/" "") +; (gtk_accel_path "<DEFAULT ROOT>/P_roof./" "") +; (gtk_accel_path "<DEFAULT ROOT>/c_ontradiction/" "") +; (gtk_accel_path "<DEFAULT ROOT>/S_et Extraction AutoInline/" "") +; (gtk_accel_path "<DEFAULT ROOT>/e_auto/" "") +; (gtk_accel_path "<DEFAULT ROOT>/d_ecompose record/" "") +; (gtk_accel_path "<DEFAULT ROOT>/f_ield/" "") +; (gtk_accel_path "<DEFAULT ROOT>/E_val/" "") +; (gtk_accel_path "<DEFAULT ROOT>/R_eset Extraction Inline/" "") diff --git a/ide/preferences.ml b/ide/preferences.ml index 499fac6f1..f10f3e503 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -199,7 +199,8 @@ let save_pref () = Config_lexer.print_file pref_file let load_pref () = - (try GtkData.AccelMap.load accel_file with _ -> ()); + GtkData.AccelMap.load (Filename.concat !Minilib.coqlib "ide/default_accel_map"); + GtkData.AccelMap.load accel_file; let p = !current in let m = Config_lexer.load_file pref_file in |