From 6858036c6d12d77df2da9643b04f56733428be13 Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 10 Jun 2011 18:35:06 +0000 Subject: 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 --- Makefile.build | 5 +- config/Makefile.template | 2 +- configure | 8 +- ide/coqide.ml | 7 +- ide/coqide_main.ml4 | 8 +- ide/coqide_ui.ml | 3 +- ide/ide_mac_stubs.c | 42 +++++- ide/mac_default_accel_map | 372 ++++++++++++++++++++++++++++++++++++++++++++++ ide/preferences.ml | 3 +- 9 files changed, 431 insertions(+), 19 deletions(-) create mode 100644 ide/mac_default_accel_map diff --git a/Makefile.build b/Makefile.build index 587be3bd79..852ce0042e 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 c5d81c9d05..e9067e98f7 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 diff --git a/configure b/configure index b43a998aad..87b773f379 100755 --- a/configure +++ b/configure @@ -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 b0fadaca2c..a57551b807 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 9a9a0a0edb..0f99648147 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 0ea018fc4d..d3543cf2ce 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -38,7 +38,7 @@ let init () = - + %s @@ -144,6 +144,7 @@ let init () = " + (if Gdk.Windowing.platform <> `QUARTZ then "" 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 87cdbf08a6..64deb71d07 100644 --- a/ide/ide_mac_stubs.c +++ b/ide/ide_mac_stubs.c @@ -4,10 +4,33 @@ #include #include +#include +#include +#include +#include #include 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 0000000000..4d34636f49 --- /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 "/C_anonical Structure/" "") +; (gtk_accel_path "/M_odule Type/" "") +; (gtk_accel_path "/c_ompute/" "") +; (gtk_accel_path "/Templates/_E.../" "") +(gtk_accel_path "/Templates/match" "c") +; (gtk_accel_path "/D_erive Inversion/" "") +; (gtk_accel_path "/Queries/Check" "F3") +; (gtk_accel_path "/i_dtac/" "") +; (gtk_accel_path "/L_oad/" "") +; (gtk_accel_path "/a_ssert/" "") +; (gtk_accel_path "/f_irstorder using/" "") +; (gtk_accel_path "/s_olve/" "") +; (gtk_accel_path "/Tactics/_l.../" "") +(gtk_accel_path "/Templates/Inductive" "i") +; (gtk_accel_path "/a_ssert (__:__)/" "") +; (gtk_accel_path "/T_est Printing Synth/" "") +; (gtk_accel_path "/Templates/_R.../" "") +; (gtk_accel_path "/Help/Browse Coq Library" "") +; (gtk_accel_path "/U_nset Extraction Optimize/" "") +; (gtk_accel_path "/s_imple inversion/" "") +(gtk_accel_path "/Edit/Copy" "c") +; (gtk_accel_path "/E_xtract Inductive/" "") +(gtk_accel_path "/Edit/Cut" "x") +; (gtk_accel_path "/i_nfo/" "") +; (gtk_accel_path "/R_emove Printing If/" "") +; (gtk_accel_path "/e_apply/" "") +; (gtk_accel_path "/F_ixpoint/" "") +; (gtk_accel_path "/c_hange __ in/" "") +; (gtk_accel_path "/l_apply/" "") +; (gtk_accel_path "/s_imple induction/" "") +; (gtk_accel_path "/f_ail/" "") +; (gtk_accel_path "/e_lim/" "") +; (gtk_accel_path "/r_ewrite <- __ in/" "") +; (gtk_accel_path "/A_dd Printing Let/" "") +; (gtk_accel_path "/T_ransparent/" "") +; (gtk_accel_path "/Tactics/_d.../" "") +(gtk_accel_path "/Tactics/Wizard" "dollar") +; (gtk_accel_path "/Windows/Detach View" "") +; (gtk_accel_path "/T_heorem/" "") +(gtk_accel_path "/Templates/Scheme" "s") +; (gtk_accel_path "/R_emark/" "") +; (gtk_accel_path "/Compile/Compile" "") +; (gtk_accel_path "/A_dd Relation/" "") +; (gtk_accel_path "/r_ename __ into/" "") +; (gtk_accel_path "/File/Save as" "") +; (gtk_accel_path "/f_irstorder/" "") +; (gtk_accel_path "/G_rammar/" "") +; (gtk_accel_path "/f_irstorder with/" "") +; (gtk_accel_path "/r_ed/" "") +; (gtk_accel_path "/D_efinition/" "") +; (gtk_accel_path "/R_equire Import/" "") +; (gtk_accel_path "/d_iscriminate/" "") +; (gtk_accel_path "/i_ntro after/" "") +; (gtk_accel_path "/Export/Latex" "") +; (gtk_accel_path "/j_p/" "") +; (gtk_accel_path "/a_uto with/" "") +; (gtk_accel_path "/S_ection/" "") +; (gtk_accel_path "/r_ewrite/" "") +; (gtk_accel_path "/Export/Html" "") +; (gtk_accel_path "/Tactics/_i.../" "") +; (gtk_accel_path "/a_utorewrite/" "") +; (gtk_accel_path "/F_ocus/" "") +; (gtk_accel_path "/Templates/_O.../" "") +; (gtk_accel_path "/l_azy in/" "") +; (gtk_accel_path "/d_ependent inversion__clear __ with/" "") +; (gtk_accel_path "/c_utrewrite/" "") +(gtk_accel_path "/Edit/Undo" "u") +; (gtk_accel_path "/c_onstructor __ with/" "") +; (gtk_accel_path "/r_ing/" "") +; (gtk_accel_path "/d_ependent rewrite <-/" "") +; (gtk_accel_path "/e_limtype/" "") +(gtk_accel_path "/Tactics/simpl" "s") +; (gtk_accel_path "/H_int/" "") +; (gtk_accel_path "/H_int Rewrite/" "") +; (gtk_accel_path "/V_ariable/" "") +; (gtk_accel_path "/U_nset Implicit Arguments/" "") +; (gtk_accel_path "/s_implify__eq/" "") +; (gtk_accel_path "/Compile/Next error" "F7") +; (gtk_accel_path "/Edit/Edit" "") +; (gtk_accel_path "/S_et Extraction Optimize/" "") +; (gtk_accel_path "/H_ypothesis/" "") +; (gtk_accel_path "/E_nd Silent./" "") +; (gtk_accel_path "/S_yntax/" "") +; (gtk_accel_path "/d_ecide equality/" "") +; (gtk_accel_path "/O_paque/" "") +; (gtk_accel_path "/Templates/_T.../" "") +; (gtk_accel_path "/Tactics/_a.../" "") +; (gtk_accel_path "/Templates/_G.../" "") +; (gtk_accel_path "/c_ase/" "") +(gtk_accel_path "/Navigation/Backward" "Up") +; (gtk_accel_path "/C_oFixpoint/" "") +; (gtk_accel_path "/P_rogram Fixpoint/" "") +; (gtk_accel_path "/d_ependent inversion__clear/" "") +; (gtk_accel_path "/c_ase __ with/" "") +; (gtk_accel_path "/a_ssumption/" "") +; (gtk_accel_path "/t_ransitivity/" "") +; (gtk_accel_path "/i_ntros until/" "") +; (gtk_accel_path "/s_plit/" "") +; (gtk_accel_path "/e_xists/" "") +(gtk_accel_path "/Templates/Theorem" "t") +; (gtk_accel_path "/Navigation/Navigation" "") +; (gtk_accel_path "/H_int Unfold/" "") +; (gtk_accel_path "/I_mplicit Arguments/" "") +; (gtk_accel_path "/Help/Help" "") +; (gtk_accel_path "/d_ecompose sum/" "") +; (gtk_accel_path "/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "") +; (gtk_accel_path "/Te_mplates/" "") +(gtk_accel_path "/Edit/Find in buffer" "f") +; (gtk_accel_path "/r_eplace __ with/" "") +(gtk_accel_path "/Tactics/omega" "o") +; (gtk_accel_path "/S_cheme/" "") +; (gtk_accel_path "/L_emma/" "") +; (gtk_accel_path "/i_nversion__clear __ in/" "") +; (gtk_accel_path "/E_xtraction Inline/" "") +; (gtk_accel_path "/S_yntactic Definition/" "") +; (gtk_accel_path "/i_nstantiate (__:=__)/" "") +; (gtk_accel_path "/C_hapter/" "") +; (gtk_accel_path "/Templates/_L.../" "") +; (gtk_accel_path "/Tactics/_f.../" "") +; (gtk_accel_path "/Queries/Queries" "") +; (gtk_accel_path "/T_est Printing Wildcard/" "") +(gtk_accel_path "/File/Open" "o") +; (gtk_accel_path "/f_old __ in/" "") +(gtk_accel_path "/Navigation/Go to" "Right") +; (gtk_accel_path "/Export/Export to" "") +; (gtk_accel_path "/c_ongruence/" "") +; (gtk_accel_path "/c_learbody/" "") +(gtk_accel_path "/File/Close buffer" "w") +; (gtk_accel_path "/a_pply/" "") +; (gtk_accel_path "/Queries/SearchAbout" "F2") +; (gtk_accel_path "/i_ntro/" "") +; (gtk_accel_path "/H_int Immediate/" "") +; (gtk_accel_path "/p_ose __:=__)/" "") +; (gtk_accel_path "/U_nset Undo/" "") +; (gtk_accel_path "/Tactics/_s.../" "") +; (gtk_accel_path "/P_rogram Definition/" "") +; (gtk_accel_path "/R_equire/" "") +; (gtk_accel_path "/c_ompare/" "") +; (gtk_accel_path "/s_ymmetry in/" "") +(gtk_accel_path "/Display/Display coercions" "c") +(gtk_accel_path "/Navigation/Previous" "less") +(gtk_accel_path "/Display/Display all low-level contents" "l") +; (gtk_accel_path "/C_oercion Local/" "") +; (gtk_accel_path "/f_ix __ with/" "") +; (gtk_accel_path "/A_dd ML Path/" "") +; (gtk_accel_path "/A_xiom/" "") +; (gtk_accel_path "/Templates/Templates" "") +; (gtk_accel_path "/a_bstract/" "") +; (gtk_accel_path "/Edit/Clear Undo Stack" "") +(gtk_accel_path "/File/New" "n") +; (gtk_accel_path "/Tactics/_hnf/" "") +; (gtk_accel_path "/d_o/" "") +; (gtk_accel_path "/E_xtract Constant/" "") +; (gtk_accel_path "/E_nd/" "") +; (gtk_accel_path "/Templates/_Qed./" "") +; (gtk_accel_path "/A_dd Rec ML Path/" "") +; (gtk_accel_path "/Templates/_D.../" "") +(gtk_accel_path "/Navigation/Hide" "h") +; (gtk_accel_path "/c_ofix/" "") +; (gtk_accel_path "/_Try Tactics/" "") +; (gtk_accel_path "/S_et Printing Wildcard/" "") +; (gtk_accel_path "/i_nversion__clear/" "") +; (gtk_accel_path "/Templates/_V.../" "") +; (gtk_accel_path "/Export/Ps" "") +; (gtk_accel_path "/U_nset Hyps__limit/" "") +; (gtk_accel_path "/H_int Extern/" "") +; (gtk_accel_path "/f_unctional induction/" "") +; (gtk_accel_path "/U_nset Extraction AutoInline/" "") +; (gtk_accel_path "/U_nfocus/" "") +; (gtk_accel_path "/Edit/External editor" "") +; (gtk_accel_path "/I_dentity Coercion/" "") +; (gtk_accel_path "/a_bsurd/" "") +; (gtk_accel_path "/c_hange/" "") +(gtk_accel_path "/Tactics/eauto" "e") +; (gtk_accel_path "/O_bligations Tactic/" "") +(gtk_accel_path "/Tactics/trivial" "v") +; (gtk_accel_path "/d_ependent inversion/" "") +; (gtk_accel_path "/c_bv/" "") +; (gtk_accel_path "/A_dd Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. /" "") +; (gtk_accel_path "/p_ose/" "") +; (gtk_accel_path "/s_et (__:=__)/" "") +; (gtk_accel_path "/R_equire Export/" "") +; (gtk_accel_path "/L_tac/" "") +; (gtk_accel_path "/A_dd Rec LoadPath/" "") +; (gtk_accel_path "/Tactics/_c.../" "") +(gtk_accel_path "/Navigation/End" "End") +(gtk_accel_path "/Templates/Lemma" "l") +(gtk_accel_path "/Navigation/Start" "Home") +; (gtk_accel_path "/Templates/_I.../" "") +(gtk_accel_path "/File/Print..." "p") +; (gtk_accel_path "/d_ependent rewrite ->/" "") +; (gtk_accel_path "/S_tructure/" "") +; (gtk_accel_path "/T_est Printing Let/" "") +; (gtk_accel_path "/T_ime/" "") +; (gtk_accel_path "/g_eneralize/" "") +(gtk_accel_path "/Display/Display all basic low-level contents" "a") +; (gtk_accel_path "/Tactics/_p.../" "") +; (gtk_accel_path "/f_old/" "") +; (gtk_accel_path "/H_int Resolve/" "") +; (gtk_accel_path "/M_utual Inductive/" "") +; (gtk_accel_path "/i_nversion __ in/" "") +; (gtk_accel_path "/Windows/Show/Hide Toolbar" "") +(gtk_accel_path "/File/Save" "s") +; (gtk_accel_path "/File/Save all" "") +; (gtk_accel_path "/Queries/Print" "F4") +; (gtk_accel_path "/c_onstructor/" "") +; (gtk_accel_path "/Export/Dvi" "") +; (gtk_accel_path "/s_etoid__replace/" "") +; (gtk_accel_path "/D_efined./" "") +; (gtk_accel_path "/I_nfix/" "") +(gtk_accel_path "/Navigation/Next" "greater") +; (gtk_accel_path "/A_dd Morphism/" "") +; (gtk_accel_path "/Windows/Windows" "") +; (gtk_accel_path "/e_xact/" "") +; (gtk_accel_path "/c_bv in/" "") +; (gtk_accel_path "/t_ry/" "") +; (gtk_accel_path "/Templates/_A.../" "") +(gtk_accel_path "/Display/Display notations" "n") +; (gtk_accel_path "/c_lear/" "") +; (gtk_accel_path "/Compile/Make" "F6") +(gtk_accel_path "/Tactics/eauto with *" "ampersand") +; (gtk_accel_path "/Help/Browse Coq Manual" "") +; (gtk_accel_path "/Templates/_N.../" "") +(gtk_accel_path "/File/Quit" "q") +; (gtk_accel_path "/u_nfold/" "") +; (gtk_accel_path "/Tactics/_u.../" "") +; (gtk_accel_path "/d_ouble induction/" "") +; (gtk_accel_path "/S_et Silent./" "") +; (gtk_accel_path "/V_ariables/" "") +; (gtk_accel_path "/U_nset Printing Wildcard/" "") +; (gtk_accel_path "/r_ewrite <-/" "") +; (gtk_accel_path "/I_nductive/" "") +; (gtk_accel_path "/e_auto with/" "") +; (gtk_accel_path "/r_epeat/" "") +; (gtk_accel_path "/Queries/Locate" "") +; (gtk_accel_path "/S_et Hyps__limit/" "") +; (gtk_accel_path "/A_dd Abstract Semi Ring A Aplus Amult Aone Azero Aeq T./" "") +; (gtk_accel_path "/c_ompute in/" "") +; (gtk_accel_path "/Templates/_F.../" "") +; (gtk_accel_path "/G_lobal Variable/" "") +; (gtk_accel_path "/t_auto/" "") +; (gtk_accel_path "/E_xtraction NoInline/" "") +; (gtk_accel_path "/u_nfold __ in/" "") +; (gtk_accel_path "/s_imple destruct/" "") +(gtk_accel_path "/Navigation/Interrupt" "Break") +; (gtk_accel_path "/Templates/_S.../" "") +; (gtk_accel_path "/i_njection/" "") +; (gtk_accel_path "/R_ead Module/" "") +; (gtk_accel_path "/P_rogram Lemma/" "") +; (gtk_accel_path "/U_nset Silent./" "") +(gtk_accel_path "/Display/Display universe levels" "u") +; (gtk_accel_path "/f_ourier/" "") +; (gtk_accel_path "/D_erive Inversion__clear/" "") +; (gtk_accel_path "/Tactics/_omega/" "") +; (gtk_accel_path "/S_et Undo/" "") +; (gtk_accel_path "/A_dd Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]./" "") +; (gtk_accel_path "/s_impl __ in/" "") +; (gtk_accel_path "/Windows/Show/Hide Query Pane" "Escape") +; (gtk_accel_path "/R_estore State/" "") +; (gtk_accel_path "/R_emove Printing Let/" "") +; (gtk_accel_path "/A_dd Printing If/" "") +(gtk_accel_path "/Tactics/tauto" "p") +; (gtk_accel_path "/s_impl/" "") +; (gtk_accel_path "/i_ntros/" "") +; (gtk_accel_path "/s_ymmetry/" "") +; (gtk_accel_path "/c_ut/" "") +; (gtk_accel_path "/r_efine/" "") +; (gtk_accel_path "/Tactics/_e.../" "") +; (gtk_accel_path "/e_exact/" "") +(gtk_accel_path "/Navigation/Forward" "Down") +(gtk_accel_path "/Edit/Paste" "v") +; (gtk_accel_path "/C_oercion/" "") +; (gtk_accel_path "/Tactics/_r.../" "") +; (gtk_accel_path "/d_estruct/" "") +; (gtk_accel_path "/A_dd Setoid/" "") +; (gtk_accel_path "/Queries/Whelp Locate" "") +; (gtk_accel_path "/T_est Printing If/" "") +; (gtk_accel_path "/Display/Display" "") +; (gtk_accel_path "/Tactics/_move __ after/" "") +(gtk_accel_path "/Edit/Complete Word" "slash") +; (gtk_accel_path "/s_ubst/" "") +; (gtk_accel_path "/Help/About Coq" "") +; (gtk_accel_path "/s_etoid__rewrite/" "") +; (gtk_accel_path "/Tactics/Try Tactics" "") +; (gtk_accel_path "/Templates/_C.../" "") +; (gtk_accel_path "/L_ocal/" "") +; (gtk_accel_path "/s_et/" "") +; (gtk_accel_path "/Tactics/_quote/" "") +(gtk_accel_path "/Templates/Definition" "d") +; (gtk_accel_path "/S_et Implicit Arguments/" "") +; (gtk_accel_path "/File/Revert all buffers" "") +; (gtk_accel_path "/Templates/_P.../" "") +; (gtk_accel_path "/t_rivial/" "") +(gtk_accel_path "/Display/Display existential variable instances" "e") +; (gtk_accel_path "/Tactics/_j.../" "") +; (gtk_accel_path "/A_dd LoadPath/" "") +; (gtk_accel_path "/N_otation/" "") +; (gtk_accel_path "/Edit/Preferences" "") +; (gtk_accel_path "/L_oad Verbose/" "") +; (gtk_accel_path "/i_ntro __ after/" "") +; (gtk_accel_path "/D_erive Dependent Inversion/" "") +; (gtk_accel_path "/d_ependent inversion __ with/" "") +; (gtk_accel_path "/P_rogram Theorem/" "") +; (gtk_accel_path "/E_xtraction Language/" "") +; (gtk_accel_path "/Templates/_U.../" "") +(gtk_accel_path "/Display/Display raw matching expressions" "m") +; (gtk_accel_path "/c_asetype/" "") +(gtk_accel_path "/Edit/Find backwards" "b") +; (gtk_accel_path "/S_ave./" "") +; (gtk_accel_path "/p_attern/" "") +; (gtk_accel_path "/M_odule/" "") +; (gtk_accel_path "/D_eclare ML Module/" "") +; (gtk_accel_path "/Templates/_H.../" "") +; (gtk_accel_path "/F_act/" "") +; (gtk_accel_path "/A_dd Field/" "") +; (gtk_accel_path "/R_emove LoadPath/" "") +; (gtk_accel_path "/Templates/_Write State/" "") +; (gtk_accel_path "/Compile/Make makefile" "") +; (gtk_accel_path "/C_oInductive/" "") +; (gtk_accel_path "/Compile/Compile buffer" "") +; (gtk_accel_path "/l_eft/" "") +; (gtk_accel_path "/a_pply __ with/" "") +(gtk_accel_path "/File/Rehighlight" "l") +; (gtk_accel_path "/File/File" "") +; (gtk_accel_path "/D_erive Dependent Inversion__clear/" "") +; (gtk_accel_path "/d_ecompose/" "") +; (gtk_accel_path "/r_ewrite __ in/" "") +(gtk_accel_path "/Display/Display implicit arguments" "i") +; (gtk_accel_path "/e_lim __ using/" "") +; (gtk_accel_path "/a_ssert (__:=__)/" "") +; (gtk_accel_path "/i_nversion __ using/" "") +; (gtk_accel_path "/P_arameter/" "") +; (gtk_accel_path "/H_int Constructors/" "") +; (gtk_accel_path "/j_p /" "") +; (gtk_accel_path "/p_rogress/" "") +; (gtk_accel_path "/Templates/_M.../" "") +; (gtk_accel_path "/e_lim __ with/" "") +; (gtk_accel_path "/f_irst/" "") +; (gtk_accel_path "/l_azy/" "") +; (gtk_accel_path "/i_nversion/" "") +(gtk_accel_path "/Help/Help for keyword" "h") +; (gtk_accel_path "/a_uto/" "") +; (gtk_accel_path "/G_oal/" "") +; (gtk_accel_path "/i_nversion __ using __ in/" "") +(gtk_accel_path "/Tactics/intuition" "i") +; (gtk_accel_path "/r_ed in/" "") +; (gtk_accel_path "/Tactics/_g.../" "") +; (gtk_accel_path "/g_eneralize dependent/" "") +; (gtk_accel_path "/Queries/About" "F5") +; (gtk_accel_path "/r_ight/" "") +(gtk_accel_path "/Tactics/auto" "a") +(gtk_accel_path "/Templates/Fixpoint" "f") +; (gtk_accel_path "/r_eflexivity/" "") +; (gtk_accel_path "/i_nduction/" "") +; (gtk_accel_path "/i_ntuition/" "") +; (gtk_accel_path "/Tactics/_t.../" "") +; (gtk_accel_path "/f_ix/" "") +; (gtk_accel_path "/Export/Pdf" "") +; (gtk_accel_path "/N_ext Obligation/" "") +(gtk_accel_path "/Tactics/auto with *" "asterisk") +; (gtk_accel_path "/R_ecord/" "") +; (gtk_accel_path "/P_roof./" "") +; (gtk_accel_path "/c_ontradiction/" "") +; (gtk_accel_path "/S_et Extraction AutoInline/" "") +; (gtk_accel_path "/e_auto/" "") +; (gtk_accel_path "/d_ecompose record/" "") +; (gtk_accel_path "/f_ield/" "") +; (gtk_accel_path "/E_val/" "") +; (gtk_accel_path "/R_eset Extraction Inline/" "") diff --git a/ide/preferences.ml b/ide/preferences.ml index 499fac6f1d..f10f3e5033 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 -- cgit v1.2.3