From a088d03434417e935df3c75f81a954eadbdfc2b8 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Mon, 21 Jul 2014 15:50:20 +0200 Subject: A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundle The created bundle contains only coqide and gtk (no coqtop, no stdlib) --- Makefile | 1 + Makefile.build | 91 +++++++- Makefile.common | 11 + ide/MacOS/Info.plist.template | 87 ++++++++ ide/MacOS/coqfile.icns | Bin 0 -> 50724 bytes ide/MacOS/coqide.icns | Bin 0 -> 38372 bytes ide/MacOS/default_accel_map | 378 +++++++++++++++++++++++++++++++++ ide/MacOS/relatify_with-respect-to_.sh | 15 ++ ide/mac_default_accel_map | 378 --------------------------------- 9 files changed, 581 insertions(+), 380 deletions(-) create mode 100644 ide/MacOS/Info.plist.template create mode 100644 ide/MacOS/coqfile.icns create mode 100644 ide/MacOS/coqide.icns create mode 100644 ide/MacOS/default_accel_map create mode 100755 ide/MacOS/relatify_with-respect-to_.sh delete mode 100644 ide/mac_default_accel_map diff --git a/Makefile b/Makefile index 17cfec0463..31b36c792e 100644 --- a/Makefile +++ b/Makefile @@ -224,6 +224,7 @@ clean-ide: rm -f ide/input_method_lexer.ml rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f ide/utf8_convert.ml + rm -rf $(COQIDEAPP) ml4clean: rm -f $(GENML4FILES) diff --git a/Makefile.build b/Makefile.build index 1a16dd6eec..dd1c30a236 100644 --- a/Makefile.build +++ b/Makefile.build @@ -297,7 +297,7 @@ COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) -thread .SUFFIXES:.vo -IDEFILES=$(wildcard ide/coq*.lang) ide/coq_style.xml ide/coq.png ide/mac_default_accel_map +IDEFILES=$(wildcard ide/coq*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map coqide-binaries: coqide-$(HASCOQIDE) coqide-no: @@ -350,7 +350,7 @@ ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) endif -install-ide-files: +install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) @@ -360,6 +360,93 @@ install-ide-info: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde +########################################################################### +# CoqIde MacOS special targets +########################################################################### + +.PHONY: $(COQIDEAPP)/Contents + +$(COQIDEAPP)/Contents: + rm -rdf $@ + $(MKDIR) $@ + sed -e "s/VERSION/$(VERSION)/g" ide/MacOS/Info.plist.template > $@/Info.plist + $(MKDIR) "$@/MacOS" + +$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ + unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \ + $(IDEFLAGS:.cma=.cmxa) $^ + $(STRIP) $@ + +$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents + $(MKDIR) $@/coq/ + $(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $@/coq/ + $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ + cp -R "$(GTKSHARE)/"locale $@ + cp -R "$(GTKSHARE)/"icons $@ + cp -R "$(GTKSHARE)/"themes $@ + +$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@ + +$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@ + + +$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib + $(MKDIR) $@/xdg/coq + $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys + $(MKDIR) $@/gtk-2.0 + { "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ + sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gdk-pixbuf.loaders + { "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\ + sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ + sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gtk-immodules.loaders + $(MKDIR) $@/pango + echo "[Pango]" > $@/pango/pangorc + +$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) + $(MKDIR) $@ + $(INSTALLLIB) $(GTKLIBS)/charset.alias $@/ + $(MKDIR) $@/pango/1.8.0/modules + $(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/ + { "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\ + sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \ + > $@/pango/1.8.0/modules.cache + + for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$i $@/; \ + ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \ + done + for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \ + do \ + for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \ + done + EXTRAWORK=1; \ + while [ $${EXTRAWORK} -eq 1 ]; \ + do EXTRAWORK=0; \ + for i in $@/*.dylib; \ + do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + done; \ + done + ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@ + +$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share + $(INSTALLLIB) ide/MacOS/*.icns $@ + +$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources + codesign -s - $@ + ########################################################################### # tests ########################################################################### diff --git a/Makefile.common b/Makefile.common index 8a70273ad0..4bc203197c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -43,6 +43,8 @@ MKDIR:=install -d COQIDEBYTE:=bin/coqide.byte$(EXE) COQIDE:=bin/coqide$(EXE) +COQIDEAPP:=bin/CoqIDE_$(VERSION).app +COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide ifeq ($(BEST),opt) OPT:=opt @@ -362,6 +364,15 @@ DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ DOT=dot ODOCDOTOPTS=-dot -dot-reduce +########################################################################### +# GTK for Coqide MacOS bundle +########################################################################### + +GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share +GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin +GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) + + # For emacs: # Local Variables: # mode: makefile diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template new file mode 100644 index 0000000000..cba708e946 --- /dev/null +++ b/ide/MacOS/Info.plist.template @@ -0,0 +1,87 @@ + + + + + CFBundleDocumentTypes + + + CFBundleTypeExtensions + + * + + CFBundleTypeName + NSStringPboardType + CFBundleTypeOSTypes + + **** + + CFBundleTypeRole + Editor + + + CFBundleTypeIconFile + coqfile.icns + CFBundleTypeName + Coq file + CFBundleTypeRole + Editor + CFBundleTypeMIMETypes + + text/plain + + CFBundleTypeExtensions + + v + + LSHandlerRank + Owner + + + CFBundleTypeName + All + CFBundleTypeRole + Editor + CFBundleTypeMIMETypes + + text/plain + + LSHandlerRank + Default + CFBundleTypeExtensions + + * + + + + CFBundleIconFile + coqide.icns + CFBundleVersion + 390 + CFBundleName + CoqIDE + CFBundleShortVersionString + Coq_vVERSION + CFBundleDisplayName + Coq Proof Assistant vVERSION + CFBundleGetInfoString + Coq_vVERSION + NSHumanReadableCopyright + Copyright 1999-2014, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS + CFBundleHelpBookFolder + share/doc/coq/html/ + CFAppleHelpAnchor + index + CFBundleExecutable + coqide + CFBundlePackageType + APPL + CFBundleInfoDictionaryVersion + 6.0 + CFBundleIdentifier + fr.inria.coqide + CFBundleDevelopmentRegion + English + NSPrincipalClass + NSApplication + + diff --git a/ide/MacOS/coqfile.icns b/ide/MacOS/coqfile.icns new file mode 100644 index 0000000000..1946f3d619 Binary files /dev/null and b/ide/MacOS/coqfile.icns differ diff --git a/ide/MacOS/coqide.icns b/ide/MacOS/coqide.icns new file mode 100644 index 0000000000..2252bb4b64 Binary files /dev/null and b/ide/MacOS/coqide.icns differ diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map new file mode 100644 index 0000000000..6f474eb124 --- /dev/null +++ b/ide/MacOS/default_accel_map @@ -0,0 +1,378 @@ +; 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/auto" "a") +; (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/auto with *" "asterisk") +; (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 "/Tactics/eauto with *" "ampersand") +; (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/Try Tactics" "") +; (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 "/Tactics/Wizard" "dollar") +; (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 "/Tactics/Tactic fourier" "") +; (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" "VoidSymbol") +; (gtk_accel_path "/Export/Html" "") +; (gtk_accel_path "/Templates/Template Extraction Inline" "") +; (gtk_accel_path "/Tactics/Tactic absurd" "") +(gtk_accel_path "/Tactics/intuition" "i") +; (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 "/Queries/Whelp Locate" "") +(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/omega" "o") +; (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/simpl" "s") +; (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/trivial" "v") +; (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 "/Tactics/eauto" "e") +; (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/MacOS/relatify_with-respect-to_.sh b/ide/MacOS/relatify_with-respect-to_.sh new file mode 100755 index 0000000000..a24af93958 --- /dev/null +++ b/ide/MacOS/relatify_with-respect-to_.sh @@ -0,0 +1,15 @@ +#!/bin/sh + +set -e + +for i in "$3/"*.dylib +do install_name_tool -change "$2"/$(basename $i) @executable_path/../Resources/lib/$(basename $i) "$1" +done +case "$1" in + *.dylib) + install_name_tool -id @executable_path/../Resources/lib/$(basename $1) $1 + for i in "$3"/*.dylib + do install_name_tool -change "$2/"$(basename $1) @executable_path/../Resources/lib/$(basename $1) $i + done;; + *) +esac diff --git a/ide/mac_default_accel_map b/ide/mac_default_accel_map deleted file mode 100644 index 6f474eb124..0000000000 --- a/ide/mac_default_accel_map +++ /dev/null @@ -1,378 +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/auto" "a") -; (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/auto with *" "asterisk") -; (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 "/Tactics/eauto with *" "ampersand") -; (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/Try Tactics" "") -; (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 "/Tactics/Wizard" "dollar") -; (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 "/Tactics/Tactic fourier" "") -; (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" "VoidSymbol") -; (gtk_accel_path "/Export/Html" "") -; (gtk_accel_path "/Templates/Template Extraction Inline" "") -; (gtk_accel_path "/Tactics/Tactic absurd" "") -(gtk_accel_path "/Tactics/intuition" "i") -; (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 "/Queries/Whelp Locate" "") -(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/omega" "o") -; (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/simpl" "s") -; (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/trivial" "v") -; (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 "/Tactics/eauto" "e") -; (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" "") -- cgit v1.2.3