blob: 017f412474b08af15c3ed761141e89629d911f97 (
plain)
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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
#!/bin/sh
#
# Simple shell script for launching Proof General.
#
# Set EMACS to override choice of Emacs version
# (otherwise script chooses emacs in preference to xemacs)
#
# 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
#
# 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.
# NB: no trailing backslash here!
PGHOMEDEFAULT=$HOME/ProofGeneral
# Try to find a default Emacs executable
if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
if which emacs > /dev/null; then
EMACS=`which emacs`
else
EMACS=`which xemacs`
fi
fi
NAME=`basename $0`
HELP="Usage: proofgeneral [OPTION] [FILE]...
Launches Emacs Proof General, editing the proof script FILE.
Options:
--emacs startup Proof General with emacs (GNU Emacs)
--xemacs startup Proof General with xemacs (XEmacs)
--emacsbin <EMACS> startup Proof General with emacs binary <EMACS>
-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 to <da+pg-bugs@inf.ed.ac.uk>."
#
VERSIONBLURB='David Aspinall.
Copyright (C) 1998-2005 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;;
-v)
VERSION=`grep proof-general-version $PGHOME/generic/proof-site.el | sed -e 's/.*Version //g' | sed -e 's/\. .*//g'`
echo "$NAME" "($VERSION)"
echo "$VERSIONBLURB"
exit 0;;
--version)
VERSION=`grep proof-general-version $PGHOME/generic/proof-site.el | sed -e 's/.*Version //g' | sed -e 's/\. .*//g'`
echo "$NAME" "($VERSION)"
echo "$VERSIONBLURB"
exit 0;;
--emacs)
EMACS=`which emacs`;;
--xemacs)
EMACS=`which xemacs`;;
--emacsbin)
EMACS=$2
shift;;
*) break;;
esac
do shift; done
if [ ! -x "$EMACS" ]; then
echo "$NAME: cannot find an Emacs or XEmacs executable. Set EMACS or your PATH." 1>&2
exit 1
fi
EMACSVERSION=`basename $EMACS`
# Try to find Proof General directory
if [ -d $PGHOMEDEFAULT ]; then
PGHOME=$PGHOMEDEFAULT
elif [ -d /usr/share/${EMACSVERSION}/site-lisp/proofgeneral ]; then
PGHOME=/usr/share/${EMACSVERSION}/site-lisp/proofgeneral
else
echo "Cannot find the Proof General lisp files: please set PGHOMEDEFAULT"
exit 1
fi
# Deal with UTF issue
if [ `locale | grep LC_CTYPE | grep UTF` ]; then
echo "Warning: detected Unicode LC_CTYPE setting, switched back to C"
echo " See FAQ for more details."
export LC_CTYPE=C
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 "$@"
|
