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
|
#!/usr/bin/env bash
#
# DESCRIPTION: Use Isabelle server when executing command
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] COMMAND"
echo
echo " Options are:"
echo " -d include session directory"
echo " -i include session"
echo " -s name of session (default Why3)"
echo
echo "Use Isabelle server when executing COMMAND."
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## main
SESSION_DIRS=()
INCLUDE_SESSIONS=()
SESSION=Why3
while getopts "d:i:s:" OPT
do
case "$OPT" in
s)
SESSION="$OPTARG"
;;
d)
SESSION_DIRS+=("-d" "$OPTARG")
;;
i)
INCLUDE_SESSIONS+=("-i" "$OPTARG")
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
SERVER=$("$ISABELLE_TOOL" server -s)
if [ $? -ne 0 ]
then
exit 2
fi
TMP1=${SERVER##[^=]*= }
ISABELLE_ADDRESS=${TMP1%%:[^:]*}
TMP2=${TMP1##[^:]*:}
ISABELLE_PORT=${TMP2%% [^ ]*}
TMP3=${TMP2##[^ ]* (password \"}
ISABELLE_PASSWORD=${TMP3%%\"[^\"]*}
export ISABELLE_ADDRESS
export ISABELLE_PORT
export ISABELLE_PASSWORD
ISABELLE_SESSION_ID=$(isabelle_client "${SESSION_DIRS[@]}" "${INCLUDE_SESSIONS[@]}" -s "${SESSION}")
if [ $? -ne 0 ]
then
fail "$ISABELLE_SESSION_ID"
fi
export ISABELLE_SESSION_ID
"$@"
RET1=$?
isabelle_client -x
RET2=$?
if [ $RET1 -ne 0 ]
then
exit $RET1
else
exit $RET2
fi
|
