1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
#!/bin/sh
#
# Simple shell script for launching Proof General.
#
# Set EMACS to override choice of Emacs version
#
# PGHOME must be set to the directory where the lisp files of Proof
# General are installed. Script checks standard locations in
# /usr/share/emacs/site-lisp, or uses PGHOMEDEFAULT defined at top.
#
# We load ~/.proofgeneral instead of ~/.emacs if it exists.
#
# Thanks to Achim Brucker for suggestions.
#
# $Id$
#
# The default path should work if you are using the Proof General RPM
# or unpack Proof General in your home directory. Otherwise edit below.
# NB: no trailing backslash here!
# On Mac, maybe:
# /Applications/Emacs.app/Contents/MacOS/Emacs/site-lisp/ProofGeneral
PGHOMEDEFAULT=$HOME/ProofGeneral
NAME=`basename $0`
HELP="Usage: proofgeneral [OPTION] [FILE]...
Launches Emacs Proof General, editing the proof script FILE.
Options:
--emacs <EMACS> startup Proof General with emacs binary <EMACS>
--pghome <PGDIR> startup Proof General from directory PGDIR
-h, --help show this help and exit
-v, --version output version information and exit
Unrecognized options are passed to Emacs, along with file names.
Examples:
$NAME Example.thy Load Proof General editing Isar file Example.thy
$NAME example.v Load Proof General editing Coq file Example.v
For documentation and latest versions, visit http://proofgeneral.inf.ed.ac.uk
Report bugs at http://proofgeneral.inf.ed.ac.uk/trac"
VERSIONBLURB='David Aspinall.
Copyright (C) 1998-2009 LFCS, University of Edinburgh, UK.
This is free software; see the source for copying conditions.'
while
case $1 in
-h)
echo "$HELP"
exit 0;;
--help)
echo "$HELP"
exit 0;;
--emacs)
EMACS="$2"
shift;;
--pghome)
PGHOME="$2"
shift;;
--version|-v)
VERSION=`grep proof-general-version $PGHOME/generic/proof-site.el | head -1 | sed -e 's/.*Version //g' | sed -e 's/\. .*//g'`
echo "$NAME" "--- script to launch Proof General $VERSION"
echo "$VERSIONBLURB"
exit 0;;
*) break;;
esac
do shift; done
# Try to find Proof General directory
if [ -z "$PGHOME" ] || [ ! -d "$PGHOME" ]; then
# default relative to this script, otherwise PGHOMEDEFAULT
MYDIR="`readlink --canonicalize "$0" | sed -ne 's,/bin/proofgeneral$,,p'`"
if [ -d "$MYDIR/generic" ]; then
PGHOME="$MYDIR"
elif [ -d "$PGHOMEDEFAULT" ]; then
PGHOME="$PGHOMEDEFAULT"
else
echo "Cannot find the Proof General lisp files: Set PGHOME or use --pghome."
exit 1
fi
fi
# Try to find an Emacs executable
if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
if which emacs > /dev/null; then
EMACS=`which emacs`
else
echo "$NAME: cannot find an Emacs executable. Change PATH, set EMACS, use --emacs to specify." 1>&2
exit 1
fi
fi
# User may use .proofgeneral in preference to .emacs or .xemacs/init.el
if [ -f $HOME/.proofgeneral ]; then
STARTUP="-q -l $HOME/.proofgeneral"
else
STARTUP=""
fi
exec $EMACS $STARTUP -eval "(or (featurep (quote proof-site)) (load \"$PGHOME/generic/proof-site.el\"))" -f proof-splash-display-screen "$@"
|
