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)
---
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 ++
5 files changed, 480 insertions(+)
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
(limited to 'ide/MacOS')
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" "