From d338a42c261287439dd6e9bc07b40a68f2a71786 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 26 Sep 2018 22:18:00 +0200 Subject: Moving configuration of coqide.keys to the coqide executable. --- .gitignore | 2 + Makefile.ide | 5 +- ide/MacOS/default_accel_map | 366 -------------------------------------------- ide/preferences.ml | 17 +- 4 files changed, 12 insertions(+), 378 deletions(-) delete mode 100644 ide/MacOS/default_accel_map diff --git a/.gitignore b/.gitignore index 93b874eae3..587a6191ab 100644 --- a/.gitignore +++ b/.gitignore @@ -191,3 +191,5 @@ theories/*/*/*/dune /user-contrib/Ltac2/dune *.install !Makefile.install + +ide/coqide.keys diff --git a/Makefile.ide b/Makefile.ide index 0a11f83a18..081d15a1a2 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -59,7 +59,7 @@ IDEBINDINGS:=ide/default.bindings IDEBINDINGSSRC:=ide/default_bindings_src.ml IDEBINDINGSEXE:=ide/default_bindings_src.exe -IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map $(IDEBINDINGS) +IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png $(IDEBINDINGS) ## GTK for Coqide MacOS bundle @@ -175,7 +175,6 @@ $(IDEBINDINGSEXE): $(IDEBINDINGSSRC) $(IDEBINDINGS): $(IDEBINDINGSEXE) $< $@ - #################### ## Install targets #################### @@ -224,7 +223,6 @@ install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same t $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) - if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi install-ide-info: $(MKDIR) $(FULLDOCDIR) @@ -271,7 +269,6 @@ $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib $(MKDIR) $@/xdg/coq - $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys $(MKDIR) $@/gtk-3.0 { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map deleted file mode 100644 index 4093d2012b..0000000000 --- a/ide/MacOS/default_accel_map +++ /dev/null @@ -1,366 +0,0 @@ -; coqide GtkAccelMap rc-file -*- scheme -*- -; this file is an automated accelerator map dump -; -; (gtk_accel_path "/Templates/Template Read Module" "") -; (gtk_accel_path "/Tactics/Tactic pattern" "") -(gtk_accel_path "/Templates/Definition" "d") -; (gtk_accel_path "/Templates/Template Program Lemma" "") -(gtk_accel_path "/Templates/Lemma" "l") -; (gtk_accel_path "/Templates/Template Fact" "") -; (gtk_accel_path "/Tactics/Tactic fold" "") -; (gtk_accel_path "/Help/About Coq" "") -; (gtk_accel_path "/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "") -; (gtk_accel_path "/Templates/Template Hypothesis" "") -; (gtk_accel_path "/Tactics/Tactic repeat" "") -; (gtk_accel_path "/Templates/Template Unset Extraction Optimize" "") -; (gtk_accel_path "/Templates/Template Add Printing Constructor" "") -; (gtk_accel_path "/Windows/Detach View" "") -; (gtk_accel_path "/Tactics/Tactic inversion" "") -; (gtk_accel_path "/Templates/Template Write State" "") -; (gtk_accel_path "/Export/Export to" "") -; (gtk_accel_path "/Tactics/Tactic inversion--clear" "") -; (gtk_accel_path "/Templates/Template Implicit Arguments" "") -; (gtk_accel_path "/Edit/Copy" "c") -; (gtk_accel_path "/Tactics/Tactic inversion -- using" "") -; (gtk_accel_path "/View/Previous tab" "Left") -; (gtk_accel_path "/Tactics/Tactic change -- in" "") -; (gtk_accel_path "/Tactics/Tactic jp" "") -; (gtk_accel_path "/Tactics/Tactic red" "") -; (gtk_accel_path "/Templates/Template Coercion" "") -; (gtk_accel_path "/Templates/Template CoFixpoint" "") -; (gtk_accel_path "/Tactics/Tactic intros until" "") -; (gtk_accel_path "/Templates/Template Derive Dependent Inversion" "") -; (gtk_accel_path "/Tactics/Tactic eapply" "") -; (gtk_accel_path "/View/View" "") -; (gtk_accel_path "/Tactics/Tactic change" "") -; (gtk_accel_path "/Tactics/Tactic firstorder using" "") -; (gtk_accel_path "/Tactics/Tactic decompose sum" "") -; (gtk_accel_path "/Tactics/Tactic cut" "") -; (gtk_accel_path "/Templates/Template Remove Printing Let" "") -; (gtk_accel_path "/Templates/Template Structure" "") -; (gtk_accel_path "/Tactics/Tactic compute in" "") -; (gtk_accel_path "/Queries/Locate" "") -; (gtk_accel_path "/Templates/Template Save." "") -; (gtk_accel_path "/Templates/Template Canonical Structure" "") -; (gtk_accel_path "/Tactics/Tactic compare" "") -; (gtk_accel_path "/Templates/Template Next Obligation" "") -(gtk_accel_path "/View/Display notations" "n") -; (gtk_accel_path "/Tactics/Tactic fail" "") -; (gtk_accel_path "/Tactics/Tactic left" "") -; (gtk_accel_path "/Edit/Undo" "u") -; (gtk_accel_path "/Templates/Template Infix" "") -; (gtk_accel_path "/Tactics/Tactic functional induction" "") -; (gtk_accel_path "/Tactics/Tactic clear" "") -; (gtk_accel_path "/Templates/Template End Silent." "") -; (gtk_accel_path "/Tactics/Tactic intros" "") -; (gtk_accel_path "/Tactics/Tactic constructor -- with" "") -; (gtk_accel_path "/Tactics/Tactic destruct" "") -; (gtk_accel_path "/Tactics/Tactic intro after" "") -; (gtk_accel_path "/Tactics/Tactic abstract" "") -; (gtk_accel_path "/Compile/Compile buffer" "") -; (gtk_accel_path "/Queries/About" "F5") -; (gtk_accel_path "/Templates/Template CoInductive" "") -; (gtk_accel_path "/Templates/Template Test Printing Wildcard" "") -; (gtk_accel_path "/Templates/Template Unset Hyps--limit" "") -; (gtk_accel_path "/Templates/Template Transparent" "") -; (gtk_accel_path "/Export/Ps" "") -; (gtk_accel_path "/Tactics/Tactic elim" "") -; (gtk_accel_path "/Templates/Template Extract Constant" "") -; (gtk_accel_path "/Tactics/Tactic assert (--:--)" "") -; (gtk_accel_path "/Templates/Template Add Rec LoadPath" "") -; (gtk_accel_path "/Edit/Redo" "") -; (gtk_accel_path "/Tactics/Tactic compute" "") -; (gtk_accel_path "/Compile/Next error" "F7") -; (gtk_accel_path "/Templates/Template Add ML Path" "") -; (gtk_accel_path "/Templates/Template Test Printing If" "") -; (gtk_accel_path "/Templates/Template Load Verbose" "") -; (gtk_accel_path "/Templates/Template Reset Extraction Inline" "") -; (gtk_accel_path "/Templates/Template Set Implicit Arguments" "") -; (gtk_accel_path "/Templates/Template Test Printing Let" "") -; (gtk_accel_path "/Windows/Windows" "") -; (gtk_accel_path "/Templates/Template Defined." "") -(gtk_accel_path "/Templates/match" "c") -; (gtk_accel_path "/Tactics/Tactic set (--:=--)" "") -; (gtk_accel_path "/Templates/Template Proof." "") -; (gtk_accel_path "/Compile/Make" "F6") -; (gtk_accel_path "/Templates/Template Module Type" "") -; (gtk_accel_path "/Tactics/Tactic apply -- with" "") -; (gtk_accel_path "/File/Save as" "") -; (gtk_accel_path "/Templates/Template Set Hyps--limit" "") -; (gtk_accel_path "/Templates/Template Global Variable" "") -; (gtk_accel_path "/Templates/Template Remove Printing Constructor" "") -; (gtk_accel_path "/Templates/Template Add Setoid" "") -; (gtk_accel_path "/Edit/Find Next" "F3") -; (gtk_accel_path "/Edit/Find" "f") -; (gtk_accel_path "/Templates/Template Add Relation" "") -; (gtk_accel_path "/Queries/Print" "F4") -; (gtk_accel_path "/Templates/Template Obligations Tactic" "") -; (gtk_accel_path "/Tactics/Tactic trivial" "") -; (gtk_accel_path "/Tactics/Tactic first" "") -; (gtk_accel_path "/Tactics/Tactic case" "") -; (gtk_accel_path "/Templates/Template Hint Constructors" "") -; (gtk_accel_path "/Templates/Template Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T." "") -; (gtk_accel_path "/Templates/Template Coercion Local" "") -(gtk_accel_path "/View/Show Query Pane" "Escape") -; (gtk_accel_path "/Tactics/Tactic cbv" "") -; (gtk_accel_path "/Tactics/Tactic inversion--clear -- in" "") -; (gtk_accel_path "/Templates/Template Add Rec ML Path" "") -; (gtk_accel_path "/Tactics/Tactic apply" "") -; (gtk_accel_path "/Export/Latex" "") -; (gtk_accel_path "/Tactics/Tactic inversion -- using -- in" "") -; (gtk_accel_path "/Tactics/Tactic generalize" "") -(gtk_accel_path "/Navigation/Backward" "Up") -; (gtk_accel_path "/Tactics/Tactic p" "") -(gtk_accel_path "/Navigation/Hide" "h") -; (gtk_accel_path "/File/Close buffer" "w") -; (gtk_accel_path "/Tactics/Tactic induction" "") -; (gtk_accel_path "/Tactics/Tactic eauto with" "") -(gtk_accel_path "/View/Display raw matching expressions" "m") -; (gtk_accel_path "/Tactics/Tactic d" "") -; (gtk_accel_path "/Tactics/Tactic u" "") -; (gtk_accel_path "/Templates/Templates" "") -; (gtk_accel_path "/Tactics/Tactic s" "") -; (gtk_accel_path "/Tactics/Tactic lapply" "") -; (gtk_accel_path "/Tactics/Tactic t" "") -; (gtk_accel_path "/Tactics/Tactic r" "") -; (gtk_accel_path "/Edit/Replace" "r") -; (gtk_accel_path "/Tactics/Tactic case -- with" "") -; (gtk_accel_path "/Tactics/Tactic eexact" "") -; (gtk_accel_path "/Queries/Check" "F3") -; (gtk_accel_path "/Tactics/Tactic omega" "") -; (gtk_accel_path "/File/New" "n") -; (gtk_accel_path "/Tactics/Tactic l" "") -; (gtk_accel_path "/Tactics/Tactic intro" "") -; (gtk_accel_path "/Tactics/Tactic j" "") -; (gtk_accel_path "/Tactics/Tactic i" "") -; (gtk_accel_path "/Templates/Template Definition" "") -; (gtk_accel_path "/Tactics/Tactic g" "") -; (gtk_accel_path "/Tactics/Tactic f" "") -; (gtk_accel_path "/Tactics/Tactic e" "") -; (gtk_accel_path "/Tactics/Tactic c" "") -(gtk_accel_path "/File/Rehighlight" "l") -; (gtk_accel_path "/Tactics/Tactic simple inversion" "") -; (gtk_accel_path "/Tactics/Tactic a" "") -; (gtk_accel_path "/Templates/Template Mutual Inductive" "") -; (gtk_accel_path "/Templates/Template Extraction NoInline" "") -(gtk_accel_path "/Templates/Theorem" "t") -; (gtk_accel_path "/Templates/Template Derive Dependent Inversion--clear" "") -; (gtk_accel_path "/Tactics/Tactic unfold" "") -; (gtk_accel_path "/Tactics/Tactic red in" "") -; (gtk_accel_path "/Tactics/Tactic rewrite <- -- in" "") -; (gtk_accel_path "/Templates/Template Hint Extern" "") -; (gtk_accel_path "/Templates/Template Unfocus" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear" "") -; (gtk_accel_path "/Help/Browse Coq Library" "") -; (gtk_accel_path "/Tactics/Tactic lazy" "") -; (gtk_accel_path "/Templates/Template Scheme" "") -(gtk_accel_path "/Tactics/tauto" "p") -; (gtk_accel_path "/Tactics/Tactic cutrewrite" "") -; (gtk_accel_path "/Tactics/Tactic contradiction" "") -; (gtk_accel_path "/Templates/Template Set Printing Wildcard" "") -; (gtk_accel_path "/Templates/Template Add LoadPath" "") -(gtk_accel_path "/Navigation/Previous" "less") -; (gtk_accel_path "/Templates/Template Require" "") -; (gtk_accel_path "/Tactics/Tactic simpl" "") -; (gtk_accel_path "/Templates/Template Require Import" "") -; (gtk_accel_path "/Templates/Template Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T." "") -(gtk_accel_path "/Navigation/Forward" "Down") -; (gtk_accel_path "/Tactics/Tactic rename -- into" "") -; (gtk_accel_path "/Compile/Compile" "") -; (gtk_accel_path "/File/Save all" "") -; (gtk_accel_path "/Tactics/Tactic fix" "") -; (gtk_accel_path "/Templates/Template Parameter" "") -; (gtk_accel_path "/Tactics/Tactic assert" "") -; (gtk_accel_path "/Tactics/Tactic do" "") -; (gtk_accel_path "/Tactics/Tactic ring" "") -; (gtk_accel_path "/Export/Pdf" "") -; (gtk_accel_path "/Tactics/Tactic quote" "") -; (gtk_accel_path "/Tactics/Tactic symmetry in" "") -; (gtk_accel_path "/Help/Help" "") -(gtk_accel_path "/Templates/Inductive" "i") -; (gtk_accel_path "/Tactics/Tactic idtac" "") -; (gtk_accel_path "/Templates/Template Syntax" "") -; (gtk_accel_path "/Tactics/Tactic intro -- after" "") -; (gtk_accel_path "/Tactics/Tactic fold -- in" "") -; (gtk_accel_path "/Templates/Template Program Definition" "") -; (gtk_accel_path "/Templates/Template Hint Resolve" "") -; (gtk_accel_path "/Templates/Template Set Extraction Optimize" "") -; (gtk_accel_path "/File/Revert all buffers" "") -; (gtk_accel_path "/Tactics/Tactic subst" "") -; (gtk_accel_path "/Tactics/Tactic autorewrite" "") -; (gtk_accel_path "/Tactics/Tactic pose" "") -; (gtk_accel_path "/Tactics/Tactic simplify--eq" "") -; (gtk_accel_path "/Tactics/Tactic clearbody" "") -; (gtk_accel_path "/Tactics/Tactic eauto" "") -; (gtk_accel_path "/Templates/Template Grammar" "") -; (gtk_accel_path "/Tactics/Tactic exact" "") -; (gtk_accel_path "/Templates/Template Unset Implicit Arguments" "") -; (gtk_accel_path "/Templates/Template Extract Inductive" "") -(gtk_accel_path "/View/Display implicit arguments" "i") -; (gtk_accel_path "/Tactics/Tactic symmetry" "") -; (gtk_accel_path "/Templates/Template Add Printing Let" "") -; (gtk_accel_path "/Help/Help for keyword" "h") -; (gtk_accel_path "/File/Save" "s") -; (gtk_accel_path "/Compile/Make makefile" "") -; (gtk_accel_path "/Templates/Template Remove LoadPath" "") -(gtk_accel_path "/Navigation/Interrupt" "Break") -(gtk_accel_path "/Navigation/End" "End") -; (gtk_accel_path "/Templates/Template Add Morphism" "") -; (gtk_accel_path "/Tactics/Tactic field" "") -; (gtk_accel_path "/Templates/Template Axiom" "") -; (gtk_accel_path "/Tactics/Tactic solve" "") -; (gtk_accel_path "/Tactics/Tactic casetype" "") -; (gtk_accel_path "/Tactics/Tactic cbv in" "") -; (gtk_accel_path "/Templates/Template Load" "") -; (gtk_accel_path "/Templates/Template Goal" "") -; (gtk_accel_path "/Tactics/Tactic exists" "") -; (gtk_accel_path "/Tactics/Tactic decompose record" "") -(gtk_accel_path "/Navigation/Go to" "Right") -; (gtk_accel_path "/Templates/Template Remark" "") -; (gtk_accel_path "/Templates/Template Set Undo" "") -; (gtk_accel_path "/Templates/Template Inductive" "") -; (gtk_accel_path "/Edit/Preferences" ",") -; (gtk_accel_path "/Export/Html" "") -; (gtk_accel_path "/Templates/Template Extraction Inline" "") -; (gtk_accel_path "/Tactics/Tactic absurd" "") -; (gtk_accel_path "/Tactics/Tactic simple induction" "") -; (gtk_accel_path "/Queries/Queries" "") -; (gtk_accel_path "/Tactics/Tactic rewrite -- in" "") -; (gtk_accel_path "/Templates/Template Hint Rewrite" "") -; (gtk_accel_path "/Templates/Template Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]." "") -; (gtk_accel_path "/Navigation/Navigation" "") -; (gtk_accel_path "/Help/Browse Coq Manual" "") -; (gtk_accel_path "/Tactics/Tactic transitivity" "") -; (gtk_accel_path "/Tactics/Tactic auto" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion -- with" "") -; (gtk_accel_path "/Tactics/Tactic assumption" "") -; (gtk_accel_path "/Templates/Template Notation" "") -; (gtk_accel_path "/Edit/Cut" "x") -; (gtk_accel_path "/Templates/Template Theorem" "") -; (gtk_accel_path "/Tactics/Tactic constructor" "") -; (gtk_accel_path "/Tactics/Tactic elim -- with" "") -; (gtk_accel_path "/Templates/Template Identity Coercion" "") -(gtk_accel_path "/View/Display all low-level contents" "l") -; (gtk_accel_path "/Tactics/Tactic right" "") -; (gtk_accel_path "/Edit/Find Previous" "F3") -; (gtk_accel_path "/Tactics/Tactic cofix" "") -; (gtk_accel_path "/Templates/Template Restore State" "") -; (gtk_accel_path "/Templates/Template Lemma" "") -; (gtk_accel_path "/Tactics/Tactic refine" "") -; (gtk_accel_path "/Templates/Template Section" "") -; (gtk_accel_path "/Tactics/Tactic assert (--:=--)" "") -; (gtk_accel_path "/Templates/Template Unset Printing Wildcard" "") -; (gtk_accel_path "/Tactics/Tactic progress" "") -; (gtk_accel_path "/Templates/Template Add Printing If" "") -; (gtk_accel_path "/Templates/Template Chapter" "") -(gtk_accel_path "/File/Print..." "p") -; (gtk_accel_path "/Templates/Template Record" "") -; (gtk_accel_path "/Tactics/Tactic info" "") -; (gtk_accel_path "/Tactics/Tactic firstorder with" "") -; (gtk_accel_path "/Templates/Template Hint Unfold" "") -; (gtk_accel_path "/Templates/Template Set Silent." "") -; (gtk_accel_path "/Templates/Template Program Theorem" "") -; (gtk_accel_path "/Templates/Template Declare ML Module" "") -; (gtk_accel_path "/Tactics/Tactic lazy in" "") -; (gtk_accel_path "/Tactics/Tactic unfold -- in" "") -; (gtk_accel_path "/Edit/Paste" "v") -; (gtk_accel_path "/Templates/Template Remove Printing If" "") -; (gtk_accel_path "/Tactics/Tactic intuition" "") -; (gtk_accel_path "/Queries/SearchAbout" "F2") -; (gtk_accel_path "/Tactics/Tactic dependent rewrite ->" "") -; (gtk_accel_path "/Templates/Template Module" "") -; (gtk_accel_path "/Templates/Template Unset Extraction AutoInline" "") -(gtk_accel_path "/Templates/Scheme" "s") -; (gtk_accel_path "/Templates/Template V" "") -; (gtk_accel_path "/Templates/Template Variable" "") -; (gtk_accel_path "/Tactics/Tactic decide equality" "") -; (gtk_accel_path "/Tactics/Tactic instantiate (--:=--)" "") -; (gtk_accel_path "/Templates/Template Syntactic Definition" "") -; (gtk_accel_path "/Templates/Template Set Extraction AutoInline" "") -; (gtk_accel_path "/Templates/Template Unset Undo" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion" "") -; (gtk_accel_path "/Tactics/Tactic setoid--rewrite" "") -; (gtk_accel_path "/Templates/Template Add Field" "") -; (gtk_accel_path "/Templates/Template Require Export" "") -; (gtk_accel_path "/Tactics/Tactic rewrite <-" "") -; (gtk_accel_path "/Tactics/Tactic split" "") -; (gtk_accel_path "/File/Quit" "q") -(gtk_accel_path "/View/Display existential variable instances" "e") -(gtk_accel_path "/Navigation/Start" "Home") -; (gtk_accel_path "/Tactics/Tactic dependent rewrite <-" "") -; (gtk_accel_path "/Templates/Template U" "") -; (gtk_accel_path "/Templates/Template Variables" "") -; (gtk_accel_path "/Templates/Template S" "") -; (gtk_accel_path "/Tactics/Tactic move -- after" "") -; (gtk_accel_path "/Templates/Template Unset Silent." "") -; (gtk_accel_path "/Templates/Template Local" "") -; (gtk_accel_path "/Templates/Template T" "") -; (gtk_accel_path "/Tactics/Tactic reflexivity" "") -; (gtk_accel_path "/Templates/Template R" "") -; (gtk_accel_path "/Templates/Template Time" "") -; (gtk_accel_path "/Templates/Template P" "") -; (gtk_accel_path "/Tactics/Tactic decompose" "") -; (gtk_accel_path "/Templates/Template N" "") -; (gtk_accel_path "/Templates/Template Eval" "") -; (gtk_accel_path "/Tactics/Tactic congruence" "") -; (gtk_accel_path "/Templates/Template O" "") -; (gtk_accel_path "/Templates/Template E" "") -; (gtk_accel_path "/Templates/Template I" "") -; (gtk_accel_path "/Templates/Template H" "") -; (gtk_accel_path "/Templates/Template Extraction Language" "") -; (gtk_accel_path "/Templates/Template M" "") -; (gtk_accel_path "/Templates/Template Derive Inversion" "") -; (gtk_accel_path "/Tactics/Tactic double induction" "") -; (gtk_accel_path "/Templates/Template L" "") -; (gtk_accel_path "/Templates/Template Derive Inversion--clear" "") -(gtk_accel_path "/View/Display universe levels" "u") -; (gtk_accel_path "/Templates/Template G" "") -; (gtk_accel_path "/Templates/Template F" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear -- with" "") -; (gtk_accel_path "/Templates/Template D" "") -; (gtk_accel_path "/Edit/Edit" "") -; (gtk_accel_path "/Tactics/Tactic firstorder" "") -; (gtk_accel_path "/Templates/Template C" "") -; (gtk_accel_path "/Tactics/Tactic replace -- with" "") -; (gtk_accel_path "/Templates/Template A" "") -; (gtk_accel_path "/Templates/Template Remove Printing Record" "") -; (gtk_accel_path "/Templates/Template Qed." "") -; (gtk_accel_path "/Templates/Template Program Fixpoint" "") -(gtk_accel_path "/View/Display coercions" "c") -; (gtk_accel_path "/Tactics/Tactic hnf" "") -; (gtk_accel_path "/Tactics/Tactic injection" "") -; (gtk_accel_path "/Tactics/Tactic rewrite" "") -; (gtk_accel_path "/Templates/Template Opaque" "") -; (gtk_accel_path "/Templates/Template Focus" "") -; (gtk_accel_path "/Templates/Template Ltac" "") -; (gtk_accel_path "/Tactics/Tactic simple destruct" "") -(gtk_accel_path "/View/Display all basic low-level contents" "a") -; (gtk_accel_path "/Tactics/Tactic jp " "") -; (gtk_accel_path "/Templates/Template Test Printing Synth" "") -; (gtk_accel_path "/Tactics/Tactic set" "") -; (gtk_accel_path "/Edit/External editor" "") -; (gtk_accel_path "/View/Show Toolbar" "") -; (gtk_accel_path "/Tactics/Tactic try" "") -; (gtk_accel_path "/Tactics/Tactic discriminate" "") -(gtk_accel_path "/Templates/Fixpoint" "f") -(gtk_accel_path "/Edit/Complete Word" "slash") -(gtk_accel_path "/Navigation/Next" "greater") -; (gtk_accel_path "/Tactics/Tactic elimtype" "") -; (gtk_accel_path "/Templates/Template End" "") -; (gtk_accel_path "/Templates/Template Fixpoint" "") -; (gtk_accel_path "/View/Next tab" "Right") -; (gtk_accel_path "/File/File" "") -; (gtk_accel_path "/Tactics/Tactic setoid--replace" "") -; (gtk_accel_path "/Tactics/Tactic generalize dependent" "") -; (gtk_accel_path "/Tactics/Tactic fix -- with" "") -; (gtk_accel_path "/Tactics/Tactic pose --:=--)" "") -; (gtk_accel_path "/Tactics/Tactic auto with" "") -; (gtk_accel_path "/Templates/Template Add Printing Record" "") -; (gtk_accel_path "/Tactics/Tactic inversion -- in" "") -; (gtk_accel_path "/File/Open" "o") -; (gtk_accel_path "/Tactics/Tactic elim -- using" "") -; (gtk_accel_path "/Templates/Template Hint" "") -; (gtk_accel_path "/Tactics/Tactic tauto" "") -; (gtk_accel_path "/Export/Dvi" "") -; (gtk_accel_path "/Tactics/Tactic simpl -- in" "") -; (gtk_accel_path "/Templates/Template Hint Immediate" "") diff --git a/ide/preferences.ml b/ide/preferences.ml index 10d779263b..2cc98e6927 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -321,17 +321,23 @@ let attach_modifiers (pref : string preference) prefix = in pref#connect#changed ~callback:cb +let select_arch m m_osx = + if Coq_config.arch = "Darwin" then m_osx else m + let modifier_for_navigation = - new preference ~name:["modifier_for_navigation"] ~init:"" ~repr:Repr.(string) + new preference ~name:["modifier_for_navigation"] + ~init:(select_arch "" "") ~repr:Repr.(string) let modifier_for_templates = new preference ~name:["modifier_for_templates"] ~init:"" ~repr:Repr.(string) let modifier_for_tactics = - new preference ~name:["modifier_for_tactics"] ~init:"" ~repr:Repr.(string) + new preference ~name:["modifier_for_tactics"] + ~init:(select_arch "" "") ~repr:Repr.(string) let modifier_for_display = - new preference ~name:["modifier_for_display"] ~init:"" ~repr:Repr.(string) + new preference ~name:["modifier_for_display"] + ~init:(select_arch "" "")~repr:Repr.(string) let modifier_for_queries = new preference ~name:["modifier_for_queries"] ~init:"" ~repr:Repr.(string) @@ -684,11 +690,6 @@ let load_pref_file loader warn name = try_load_pref_file loader warn old_user_file with Not_found -> (* Built-in configuration *) - try - let default_file = get_config_file [Minilib.coqide_default_config_dir ()] name in - warn ~delay:5000 ("No " ^ name ^ ", using default configuration file"); - try_load_pref_file loader warn default_file - with Not_found -> warn ~delay:5000 ("No " ^ name ^ ", using default internal configuration") let load_accel_pref ~warn = -- cgit v1.2.3