blob: 38adfa7a6955c71e925b919d7d425365ec26a7fa (
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
|
#!/bin/bash
#
# $Id$
#
# Proof General interface wrapper for Isabelle/Isar.
## diagnostics
PRG=$(basename $0)
function usage()
{
echo
echo "Usage: $PRG [OPTIONS] [FILES ...]"
echo
echo " Options are:"
echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
echo " -p NAME Emacs program name (default xemacs)"
echo " -u BOOL use .emacs file (default true)"
echo " -w BOOL use window system (default true)"
echo " -x BOOL enable x-symbol package"
echo
echo "Starts Proof General for Isabelle/Isar with proof documents FILES"
echo "(default Scratch.thy)."
echo
echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
export PROOFGENERAL_HOME=$(cd $(dirname "$0"); cd ..; echo $PWD)
# options
LOGIC="$ISABELLE_LOGIC"
PROGNAME="xemacs"
INITFILE="true"
WINDOWSYSTEM="true"
XSYMBOL=""
function getoptions()
{
OPTIND=1
while getopts "l:p:u:w:x:" OPT
do
case "$OPT" in
l)
LOGIC="$OPTARG"
;;
p)
PROGNAME="$OPTARG"
;;
u)
INITFILE="$OPTARG"
;;
w)
WINDOWSYSTEM="$OPTARG"
;;
x)
XSYMBOL="$OPTARG"
;;
\?)
usage
;;
esac
done
}
getoptions $PROOFGENERAL_OPTIONS
getoptions "$@"
shift $(($OPTIND - 1))
# args
FILES="$@"
shift $#
[ -z "$FILES" ] && FILES="Scratch.thy"
## main
ARGS=""
[ "$INITFILE" = false ] && ARGS="$ARGS -q"
if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
ARGS="$ARGS -T Isabelle"
else
ARGS="$ARGS -nw"
fi
ARGS="$ARGS -l $PROOFGENERAL_HOME/isar/interface-setup.el"
ARGS="$ARGS -l $PROOFGENERAL_HOME/generic/proof-site.el"
for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
"$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
do
[ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
done
export PROOFGENERAL_ASSISTANTS=isar
export PROOFGENERAL_LOGIC="$LOGIC"
export PROOFGENERAL_XSYMBOL="$XSYMBOL"
exec $PROGNAME $ARGS $FILES
|
