|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # interface,v 9.1 2008/02/06 15:40:45 makarius Exp |
|
4 # |
|
5 # Proof General interface wrapper for Isabelle. |
|
6 |
|
7 |
|
8 ## self references |
|
9 |
|
10 THIS="$(cd "$(dirname "$0")"; pwd)" |
|
11 SUPER="$(cd "$THIS/.."; pwd)" |
|
12 |
|
13 |
|
14 ## diagnostics |
|
15 |
|
16 usage() |
|
17 { |
|
18 echo |
|
19 echo "Usage: Isabelle [OPTIONS] [FILES ...]" |
|
20 echo |
|
21 echo " Options are:" |
|
22 echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)" |
|
23 echo " -L NAME abbreviates -l NAME -k NAME" |
|
24 echo " -P BOOL actually start Proof General (default true), otherwise" |
|
25 echo " run plain tty session" |
|
26 echo " -U BOOL enable Unicode (UTF-8) communication (default true)" |
|
27 echo " -X BOOL configure the X-Symbol package on startup (default true)" |
|
28 echo " -f SIZE set X-Symbol font size (default 12)" |
|
29 echo " -g GEOMETRY specify Emacs geometry" |
|
30 echo " -k NAME use specific isar-keywords for named logic" |
|
31 echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)" |
|
32 echo " -m MODE add print mode for output" |
|
33 echo " -p NAME Emacs program name (default emacs)" |
|
34 echo " -u BOOL use personal .emacs file (default true)" |
|
35 echo " -w BOOL use window system (default true)" |
|
36 echo " -x BOOL enable the X-Symbol package on startup (default false)" |
|
37 echo |
|
38 echo "Starts Proof General for Isabelle with theory and proof FILES" |
|
39 echo "(default Scratch.thy)." |
|
40 echo |
|
41 echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS" |
|
42 echo |
|
43 exit 1 |
|
44 } |
|
45 |
|
46 fail() |
|
47 { |
|
48 echo "$1" >&2 |
|
49 exit 2 |
|
50 } |
|
51 |
|
52 |
|
53 ## process command line |
|
54 |
|
55 # options |
|
56 |
|
57 ISABELLE_OPTIONS="" |
|
58 ISAR="true" |
|
59 START_PG="true" |
|
60 GEOMETRY="" |
|
61 KEYWORDS="" |
|
62 LOGIC="$ISABELLE_LOGIC" |
|
63 PROGNAME="emacs" |
|
64 INITFILE="true" |
|
65 WINDOWSYSTEM="true" |
|
66 XSYMBOL="" |
|
67 XSYMBOL_SETUP=true |
|
68 XSYMBOL_FONTSIZE="12" |
|
69 UNICODE="" |
|
70 |
|
71 getoptions() |
|
72 { |
|
73 OPTIND=1 |
|
74 while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT |
|
75 do |
|
76 case "$OPT" in |
|
77 I) |
|
78 ISAR="$OPTARG" |
|
79 ;; |
|
80 L) |
|
81 KEYWORDS="$OPTARG" |
|
82 LOGIC="$OPTARG" |
|
83 ;; |
|
84 P) |
|
85 START_PG="$OPTARG" |
|
86 ;; |
|
87 U) |
|
88 UNICODE="$OPTARG" |
|
89 ;; |
|
90 X) |
|
91 XSYMBOL_SETUP="$OPTARG" |
|
92 ;; |
|
93 f) |
|
94 XSYMBOL_FONTSIZE="$OPTARG" |
|
95 ;; |
|
96 g) |
|
97 GEOMETRY="$OPTARG" |
|
98 ;; |
|
99 k) |
|
100 KEYWORDS="$OPTARG" |
|
101 ;; |
|
102 l) |
|
103 LOGIC="$OPTARG" |
|
104 ;; |
|
105 m) |
|
106 if [ -z "$ISABELLE_OPTIONS" ]; then |
|
107 ISABELLE_OPTIONS="-m $OPTARG" |
|
108 else |
|
109 ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG" |
|
110 fi |
|
111 ;; |
|
112 p) |
|
113 PROGNAME="$OPTARG" |
|
114 ;; |
|
115 u) |
|
116 INITFILE="$OPTARG" |
|
117 ;; |
|
118 w) |
|
119 WINDOWSYSTEM="$OPTARG" |
|
120 ;; |
|
121 x) |
|
122 XSYMBOL="$OPTARG" |
|
123 ;; |
|
124 \?) |
|
125 usage |
|
126 ;; |
|
127 esac |
|
128 done |
|
129 } |
|
130 |
|
131 eval "OPTIONS=($PROOFGENERAL_OPTIONS)" |
|
132 getoptions "${OPTIONS[@]}" |
|
133 |
|
134 getoptions "$@" |
|
135 shift $(($OPTIND - 1)) |
|
136 |
|
137 |
|
138 # args |
|
139 |
|
140 declare -a FILES=() |
|
141 |
|
142 if [ "$#" -eq 0 ]; then |
|
143 FILES["${#FILES[@]}"]="Scratch.thy" |
|
144 else |
|
145 while [ "$#" -gt 0 ]; do |
|
146 FILES["${#FILES[@]}"]="$1" |
|
147 shift |
|
148 done |
|
149 fi |
|
150 |
|
151 |
|
152 ## smart X11 font installation |
|
153 |
|
154 function checkfonts () |
|
155 { |
|
156 XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1 |
|
157 |
|
158 case "$XLSFONTS" in |
|
159 xlsfonts:*) |
|
160 return 1 |
|
161 ;; |
|
162 esac |
|
163 |
|
164 return 0 |
|
165 } |
|
166 |
|
167 function installfonts () |
|
168 { |
|
169 checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS |
|
170 } |
|
171 |
|
172 |
|
173 ## main |
|
174 |
|
175 # Isabelle2008 compatibility |
|
176 [ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" |
|
177 [ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" |
|
178 |
|
179 if [ "$START_PG" = false ]; then |
|
180 |
|
181 [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I" |
|
182 exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC" |
|
183 |
|
184 else |
|
185 |
|
186 declare -a ARGS=() |
|
187 |
|
188 if [ -n "$GEOMETRY" ]; then |
|
189 ARGS["${#ARGS[@]}"]="-geometry" |
|
190 ARGS["${#ARGS[@]}"]="$GEOMETRY" |
|
191 fi |
|
192 |
|
193 [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" |
|
194 |
|
195 if [ "$WINDOWSYSTEM" = false ]; then |
|
196 ARGS["${#ARGS[@]}"]="-nw" |
|
197 XSYMBOL=false |
|
198 elif [ -z "$DISPLAY" ]; then |
|
199 XSYMBOL=false |
|
200 else |
|
201 [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts |
|
202 fi |
|
203 |
|
204 if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ] |
|
205 then |
|
206 if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ] |
|
207 then |
|
208 cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/" |
|
209 cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/" |
|
210 sleep 3 |
|
211 fi |
|
212 fi |
|
213 |
|
214 ARGS["${#ARGS[@]}"]="-l" |
|
215 ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" |
|
216 |
|
217 if [ -n "$KEYWORDS" ]; then |
|
218 if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then |
|
219 ARGS["${#ARGS[@]}"]="-l" |
|
220 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" |
|
221 elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then |
|
222 ARGS["${#ARGS[@]}"]="-l" |
|
223 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" |
|
224 else |
|
225 fail "No isar-keywords file for '$KEYWORDS'" |
|
226 fi |
|
227 elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then |
|
228 ARGS["${#ARGS[@]}"]="-l" |
|
229 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el" |
|
230 elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then |
|
231 ARGS["${#ARGS[@]}"]="-l" |
|
232 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" |
|
233 fi |
|
234 |
|
235 for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ |
|
236 "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" |
|
237 do |
|
238 if [ -f "$FILE" ]; then |
|
239 ARGS["${#ARGS[@]}"]="-l" |
|
240 ARGS["${#ARGS[@]}"]="$FILE" |
|
241 fi |
|
242 done |
|
243 |
|
244 case "$LOGIC" in |
|
245 /*) |
|
246 ;; |
|
247 */*) |
|
248 LOGIC="$(pwd -P)/$LOGIC" |
|
249 ;; |
|
250 esac |
|
251 |
|
252 export PROOFGENERAL_HOME="$SUPER" |
|
253 export PROOFGENERAL_ASSISTANTS="isar" |
|
254 export PROOFGENERAL_LOGIC="$LOGIC" |
|
255 export PROOFGENERAL_XSYMBOL="$XSYMBOL" |
|
256 export PROOFGENERAL_UNICODE="$UNICODE" |
|
257 |
|
258 export ISABELLE_OPTIONS XSYMBOL_FONTSIZE |
|
259 |
|
260 exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" |
|
261 |
|
262 fi |