aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build5
-rw-r--r--config/Makefile.template2
-rwxr-xr-xconfigure8
-rw-r--r--ide/coqide.ml7
-rw-r--r--ide/coqide_main.ml48
-rw-r--r--ide/coqide_ui.ml3
-rw-r--r--ide/ide_mac_stubs.c42
-rw-r--r--ide/mac_default_accel_map372
-rw-r--r--ide/preferences.ml3
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
diff --git a/configure b/configure
index b43a998aa..87b773f37 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 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 15:04:12 +0000