author | haftmann |
Tue, 21 Dec 2010 15:16:27 +0100 | |
changeset 41366 | ea73e74ec827 |
parent 40570 | bf8f92bdf630 |
child 41511 | 2fe62d602681 |
permissions | -rw-r--r-- |
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
1 |
# -*- shell-script -*- :mode=shellscript: |
29145 | 2 |
# |
9789 | 3 |
# Author: Markus Wenzel, TU Muenchen |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
4 |
# |
2348 | 5 |
# getsettings - bash source script to augment current env. |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
6 |
|
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
7 |
if [ -z "$ISABELLE_SETTINGS_PRESENT" ] |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
8 |
then |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
9 |
|
3185 | 10 |
set -o allexport |
11 |
||
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
12 |
ISABELLE_SETTINGS_PRESENT=true |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
13 |
|
15972 | 14 |
export ISABELLE_HOME |
12598 | 15 |
if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; } |
16 |
then |
|
17 |
echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!" |
|
18 |
echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\"" |
|
19 |
fi |
|
2736 | 20 |
|
11553 | 21 |
#key executables |
28499
eff93bc3c14f
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL -- old bindings stay for a while (legacy feature);
wenzelm
parents:
28055
diff
changeset
|
22 |
ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process" |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28499
diff
changeset
|
23 |
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
24 |
|
34254
14f6df4f473d
shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset
|
25 |
function isabelle () |
14f6df4f473d
shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset
|
26 |
{ |
14f6df4f473d
shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset
|
27 |
"$ISABELLE_TOOL" "$@" |
14f6df4f473d
shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset
|
28 |
} |
14f6df4f473d
shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset
|
29 |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
30 |
#platform |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
31 |
. "$ISABELLE_HOME/lib/scripts/isabelle-platform" |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
32 |
|
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
33 |
#Isabelle distribution identifier -- filled in automatically! |
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
34 |
ISABELLE_IDENTIFIER="" |
21490 | 35 |
|
2643 | 36 |
#users tend to put strange things in here ... |
2621 | 37 |
unset ENV |
38 |
unset BASH_ENV |
|
39 |
||
9680 | 40 |
#support easy settings |
41 |
function choosefrom () |
|
42 |
{ |
|
43 |
local RESULT="" |
|
44 |
local FILE="" |
|
45 |
||
46 |
for FILE in "$@" |
|
47 |
do |
|
48 |
[ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE" |
|
49 |
done |
|
50 |
||
51 |
[ -z "$RESULT" ] && RESULT="$FILE" |
|
52 |
echo "$RESULT" |
|
53 |
} |
|
54 |
||
27914 | 55 |
#JVM path wrapper |
25650 | 56 |
if [ "$OSTYPE" = cygwin ]; then |
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
57 |
CLASSPATH="$(cygpath -u -p "$CLASSPATH")" |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
58 |
function jvmpath() { cygpath -w -p "$@"; } |
36194 | 59 |
THIS_CYGWIN="$(jvmpath "/")" |
25650 | 60 |
else |
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
61 |
function jvmpath() { echo "$@"; } |
25650 | 62 |
fi |
28055
eb855c3db657
provide HOME_JVM=HOME to prevent implicit cygpath mangling;
wenzelm
parents:
27940
diff
changeset
|
63 |
HOME_JVM="$HOME" |
25650 | 64 |
|
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
65 |
#CLASSPATH convenience |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
66 |
function classpath () { |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
67 |
for X in "$@" |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
68 |
do |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
69 |
if [ -z "$CLASSPATH" ]; then |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
70 |
CLASSPATH="$X" |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
71 |
else |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
72 |
CLASSPATH="$CLASSPATH:$X" |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
73 |
fi |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
74 |
done |
40568
3003be923908
paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
wenzelm
parents:
36196
diff
changeset
|
75 |
export CLASSPATH |
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
76 |
} |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
77 |
|
32390
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
78 |
#arrays |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
79 |
function splitarray () |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
80 |
{ |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
81 |
SPLITARRAY=() |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
82 |
local IFS="$1"; shift |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
83 |
for X in $* |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
84 |
do |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
85 |
SPLITARRAY["${#SPLITARRAY[@]}"]="$X" |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
86 |
done |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
87 |
} |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
88 |
|
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
89 |
#nested components |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
90 |
ISABELLE_COMPONENTS="" |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
91 |
function init_component () |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
92 |
{ |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
93 |
local COMPONENT="$1" |
40570
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
94 |
case "$COMPONENT" in |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
95 |
/*) ;; |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
96 |
*) |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
97 |
echo >&2 "Absolute component path required: \"$COMPONENT\"" |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
98 |
exit 2 |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
99 |
;; |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
100 |
esac |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
101 |
|
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
102 |
if [ ! -d "$COMPONENT" ]; then |
33295 | 103 |
echo >&2 "Bad Isabelle component: \"$COMPONENT\"" |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
104 |
exit 2 |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
105 |
elif [ -z "$ISABELLE_COMPONENTS" ]; then |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
106 |
ISABELLE_COMPONENTS="$COMPONENT" |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
107 |
else |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
108 |
ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
109 |
fi |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
110 |
if [ -f "$COMPONENT/etc/settings" ]; then |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
111 |
source "$COMPONENT/etc/settings" || exit 2 |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
112 |
fi |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
113 |
if [ -f "$COMPONENT/etc/components" ]; then |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
114 |
{ |
33512
771ec7306438
init_component: slightly more robust read (raw input, succeed on non-terminated last line);
wenzelm
parents:
33295
diff
changeset
|
115 |
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } |
771ec7306438
init_component: slightly more robust read (raw input, succeed on non-terminated last line);
wenzelm
parents:
33295
diff
changeset
|
116 |
do |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
117 |
case "$REPLY" in |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
118 |
\#* | "") ;; |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
119 |
/*) init_component "$REPLY" ;; |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
120 |
*) init_component "$COMPONENT/$REPLY" ;; |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
121 |
esac |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
122 |
done |
33295 | 123 |
} < "$COMPONENT/etc/components" |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
124 |
fi |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
125 |
} |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
126 |
|
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
127 |
#main components |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
128 |
init_component "$ISABELLE_HOME" |
9789 | 129 |
|
130 |
[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ |
|
32321
13920dbe4547
more uniform handling of ISABELLE_HOME_USER component;
wenzelm
parents:
32305
diff
changeset
|
131 |
{ echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; } |
13920dbe4547
more uniform handling of ISABELLE_HOME_USER component;
wenzelm
parents:
32305
diff
changeset
|
132 |
[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
133 |
|
21490 | 134 |
#ML system identifier |
6413 | 135 |
if [ -z "$ML_PLATFORM" ]; then |
136 |
ML_IDENTIFIER="$ML_SYSTEM" |
|
137 |
else |
|
138 |
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
|
139 |
fi |
|
21468
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents:
16293
diff
changeset
|
140 |
|
6413 | 141 |
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
3118 | 142 |
|
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
143 |
set +o allexport |
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
144 |
|
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
145 |
fi |