1 #!/usr/bin/env bash |
|
2 # |
|
3 # Proof General interface wrapper for Isabelle. |
|
4 |
|
5 |
|
6 ## self references |
|
7 |
|
8 THIS="$(cd "$(dirname "$0")"; pwd)" |
|
9 SUPER="$(cd "$THIS/.."; pwd)" |
|
10 |
|
11 |
|
12 ## diagnostics |
|
13 |
|
14 usage() |
|
15 { |
|
16 echo |
|
17 echo "Usage: isabelle emacs [OPTIONS] [FILES ...]" |
|
18 echo |
|
19 echo " Options are:" |
|
20 echo " -L NAME abbreviates -l NAME -k NAME" |
|
21 echo " -U BOOL enable UTF-8 communication (default true)" |
|
22 echo " -f FONT specify Emacs font" |
|
23 echo " -g GEOMETRY specify Emacs geometry" |
|
24 echo " -k NAME use specific isar-keywords for named logic" |
|
25 echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)" |
|
26 echo " -m MODE add print mode for output" |
|
27 echo " -p NAME Emacs program name (default emacs)" |
|
28 echo " -u BOOL use personal .emacs file (default true)" |
|
29 echo " -w BOOL use window system (default true)" |
|
30 echo " -x BOOL render Isabelle symbols via Unicode (default false)" |
|
31 echo |
|
32 echo "Starts Proof General for Isabelle with theory and proof FILES" |
|
33 echo "(default Scratch.thy)." |
|
34 echo |
|
35 echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS" |
|
36 echo |
|
37 exit 1 |
|
38 } |
|
39 |
|
40 fail() |
|
41 { |
|
42 echo "$1" >&2 |
|
43 exit 2 |
|
44 } |
|
45 |
|
46 |
|
47 ## process command line |
|
48 |
|
49 # options |
|
50 |
|
51 ISABELLE_OPTIONS="" |
|
52 |
|
53 KEYWORDS="" |
|
54 LOGIC="$ISABELLE_LOGIC" |
|
55 UNICODE="" |
|
56 FONT="" |
|
57 GEOMETRY="" |
|
58 PROGNAME="emacs" |
|
59 INITFILE="true" |
|
60 WINDOWSYSTEM="true" |
|
61 UNICODE_SYMBOLS="" |
|
62 |
|
63 getoptions() |
|
64 { |
|
65 OPTIND=1 |
|
66 while getopts "L:U:f:g:k:l:m:p:u:w:x:" OPT |
|
67 do |
|
68 case "$OPT" in |
|
69 L) |
|
70 KEYWORDS="$OPTARG" |
|
71 LOGIC="$OPTARG" |
|
72 ;; |
|
73 U) |
|
74 UNICODE="$OPTARG" |
|
75 ;; |
|
76 f) |
|
77 FONT="$OPTARG" |
|
78 ;; |
|
79 g) |
|
80 GEOMETRY="$OPTARG" |
|
81 ;; |
|
82 k) |
|
83 KEYWORDS="$OPTARG" |
|
84 ;; |
|
85 l) |
|
86 LOGIC="$OPTARG" |
|
87 ;; |
|
88 m) |
|
89 if [ -z "$ISABELLE_OPTIONS" ]; then |
|
90 ISABELLE_OPTIONS="-m $OPTARG" |
|
91 else |
|
92 ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG" |
|
93 fi |
|
94 ;; |
|
95 p) |
|
96 PROGNAME="$OPTARG" |
|
97 ;; |
|
98 u) |
|
99 INITFILE="$OPTARG" |
|
100 ;; |
|
101 w) |
|
102 WINDOWSYSTEM="$OPTARG" |
|
103 ;; |
|
104 x) |
|
105 UNICODE_SYMBOLS="$OPTARG" |
|
106 ;; |
|
107 \?) |
|
108 usage |
|
109 ;; |
|
110 esac |
|
111 done |
|
112 } |
|
113 |
|
114 eval "OPTIONS=($PROOFGENERAL_OPTIONS)" |
|
115 getoptions "${OPTIONS[@]}" |
|
116 |
|
117 getoptions "$@" |
|
118 shift $(($OPTIND - 1)) |
|
119 |
|
120 |
|
121 # args |
|
122 |
|
123 declare -a FILES=() |
|
124 |
|
125 if [ "$#" -eq 0 ]; then |
|
126 FILES["${#FILES[@]}"]="Scratch.thy" |
|
127 else |
|
128 while [ "$#" -gt 0 ]; do |
|
129 FILES["${#FILES[@]}"]="$1" |
|
130 shift |
|
131 done |
|
132 fi |
|
133 |
|
134 |
|
135 ## main |
|
136 |
|
137 declare -a ARGS=() |
|
138 |
|
139 if [ -n "$FONT" ]; then |
|
140 ARGS["${#ARGS[@]}"]="-fn" |
|
141 ARGS["${#ARGS[@]}"]="$FONT" |
|
142 fi |
|
143 |
|
144 if [ -n "$GEOMETRY" ]; then |
|
145 ARGS["${#ARGS[@]}"]="-geometry" |
|
146 ARGS["${#ARGS[@]}"]="$GEOMETRY" |
|
147 fi |
|
148 |
|
149 [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" |
|
150 [ "$WINDOWSYSTEM" = false ] && ARGS["${#ARGS[@]}"]="-nw" |
|
151 |
|
152 ARGS["${#ARGS[@]}"]="-l" |
|
153 ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" |
|
154 |
|
155 if [ -n "$KEYWORDS" ]; then |
|
156 if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then |
|
157 ARGS["${#ARGS[@]}"]="-l" |
|
158 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" |
|
159 elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then |
|
160 ARGS["${#ARGS[@]}"]="-l" |
|
161 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" |
|
162 else |
|
163 fail "No isar-keywords file for '$KEYWORDS'" |
|
164 fi |
|
165 elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then |
|
166 ARGS["${#ARGS[@]}"]="-l" |
|
167 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el" |
|
168 elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then |
|
169 ARGS["${#ARGS[@]}"]="-l" |
|
170 ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" |
|
171 fi |
|
172 |
|
173 for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ |
|
174 "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" |
|
175 do |
|
176 if [ -f "$FILE" ]; then |
|
177 ARGS["${#ARGS[@]}"]="-l" |
|
178 ARGS["${#ARGS[@]}"]="$FILE" |
|
179 fi |
|
180 done |
|
181 |
|
182 case "$LOGIC" in |
|
183 /*) |
|
184 ;; |
|
185 */*) |
|
186 LOGIC="$(pwd -P)/$LOGIC" |
|
187 ;; |
|
188 esac |
|
189 |
|
190 export PROOFGENERAL_HOME="$SUPER" |
|
191 export PROOFGENERAL_ASSISTANTS="isar" |
|
192 export PROOFGENERAL_LOGIC="$LOGIC" |
|
193 export PROOFGENERAL_UNICODE="$UNICODE" |
|
194 export PROOFGENERAL_UNICODE_SYMBOLS="$UNICODE_SYMBOLS" |
|
195 |
|
196 export ISABELLE_OPTIONS |
|
197 |
|
198 # Isabelle2008 compatibility |
|
199 [ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" |
|
200 [ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" |
|
201 |
|
202 exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" |
|
203 |
|