| author | sultana | 
| Sat, 14 Apr 2012 23:52:17 +0100 | |
| changeset 47477 | 3fabf352243e | 
| parent 47465 | 71d5f37ee2bf | 
| child 47490 | f4348634595b | 
| 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  | 
|
| 
47461
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
14  | 
#JVM path wrapper  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
15  | 
if [ "$OSTYPE" = cygwin ]  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
16  | 
then  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
17  | 
ISABELLE_HOME_WINDOWS="$(cygpath -d "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
18  | 
ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
19  | 
|
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
20  | 
CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
21  | 
  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
 | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
22  | 
THIS_CYGWIN="$(jvmpath "/")"  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
23  | 
else  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
24  | 
  function jvmpath() { echo "$@"; }
 | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
25  | 
CLASSPATH="$CLASSPATH"  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
26  | 
fi  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
27  | 
HOME_JVM="$HOME"  | 
| 
 
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
 
wenzelm 
parents: 
47254 
diff
changeset
 | 
28  | 
|
| 15972 | 29  | 
export ISABELLE_HOME  | 
| 12598 | 30  | 
if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
 | 
31  | 
then  | 
|
| 
45094
 
a43694a0b726
tuned message, which is displayed after termination of Isabelle.app on Mac OS;
 
wenzelm 
parents: 
43519 
diff
changeset
 | 
32  | 
echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"  | 
| 12598 | 33  | 
echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""  | 
34  | 
fi  | 
|
| 2736 | 35  | 
|
| 11553 | 36  | 
#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
 | 
37  | 
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
 | 
38  | 
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"  | 
| 
2299
 
ed9720047d53
getsettings: bash source script to augment current env.
 
wenzelm 
parents:  
diff
changeset
 | 
39  | 
|
| 
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
 | 
40  | 
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
 | 
41  | 
{
 | 
| 
 
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
 | 
42  | 
"$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
 | 
43  | 
}  | 
| 
 
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
 | 
44  | 
|
| 
36196
 
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
 
wenzelm 
parents: 
36194 
diff
changeset
 | 
45  | 
#platform  | 
| 41758 | 46  | 
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"  | 
| 
36196
 
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
 
wenzelm 
parents: 
36194 
diff
changeset
 | 
47  | 
|
| 
25434
 
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
 
wenzelm 
parents: 
21490 
diff
changeset
 | 
48  | 
#Isabelle distribution identifier -- filled in automatically!  | 
| 41511 | 49  | 
ISABELLE_ID=""  | 
| 
25434
 
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
 
wenzelm 
parents: 
21490 
diff
changeset
 | 
50  | 
ISABELLE_IDENTIFIER=""  | 
| 21490 | 51  | 
|
| 41511 | 52  | 
#sometimes users put strange things in here ...  | 
| 2621 | 53  | 
unset ENV  | 
54  | 
unset BASH_ENV  | 
|
55  | 
||
| 9680 | 56  | 
#support easy settings  | 
57  | 
function choosefrom ()  | 
|
58  | 
{
 | 
|
59  | 
local RESULT=""  | 
|
60  | 
local FILE=""  | 
|
61  | 
||
62  | 
for FILE in "$@"  | 
|
63  | 
do  | 
|
64  | 
[ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"  | 
|
65  | 
done  | 
|
66  | 
||
67  | 
[ -z "$RESULT" ] && RESULT="$FILE"  | 
|
68  | 
echo "$RESULT"  | 
|
69  | 
}  | 
|
70  | 
||
| 
41614
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
71  | 
#shared library convenience  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
72  | 
function librarypath () {
 | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
73  | 
for X in "$@"  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
74  | 
do  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
75  | 
case "$ISABELLE_PLATFORM" in  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
76  | 
*-darwin)  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
77  | 
if [ -z "$DYLD_LIBRARY_PATH" ]; then  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
78  | 
DYLD_LIBRARY_PATH="$X"  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
79  | 
else  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
80  | 
DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
81  | 
fi  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
82  | 
export DYLD_LIBRARY_PATH  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
83  | 
;;  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
84  | 
*)  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
85  | 
if [ -z "$LD_LIBRARY_PATH" ]; then  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
86  | 
LD_LIBRARY_PATH="$X"  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
87  | 
else  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
88  | 
LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
89  | 
fi  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
90  | 
export LD_LIBRARY_PATH  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
91  | 
;;  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
92  | 
esac  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
93  | 
done  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
94  | 
}  | 
| 
 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
 
wenzelm 
parents: 
41511 
diff
changeset
 | 
95  | 
|
| 
47115
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
96  | 
#robust invocation via ISABELLE_JDK_HOME  | 
| 
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
97  | 
function isabelle_jdk () {
 | 
| 
47465
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
98  | 
if [ -z "$ISABELLE_JDK_HOME" ]; then  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
99  | 
echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
100  | 
return 2  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
101  | 
else  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
102  | 
local PRG="$1"; shift  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
103  | 
"$ISABELLE_JDK_HOME/bin/$PRG" "$@"  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
104  | 
fi  | 
| 
47115
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
105  | 
}  | 
| 
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
106  | 
|
| 
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
107  | 
#robust invocation via SCALA_HOME  | 
| 
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
108  | 
function isabelle_scala () {
 | 
| 
47465
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
109  | 
if [ -z "$ISABELLE_JDK_HOME" ]; then  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
110  | 
echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
111  | 
return 2  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
112  | 
elif [ -z "$SCALA_HOME" ]; then  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
113  | 
echo "Unknown SCALA_HOME -- Scala unavailable" >&2  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
114  | 
return 2  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
115  | 
else  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
116  | 
local PRG="$1"; shift  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
117  | 
"$SCALA_HOME/bin/$PRG" "$@"  | 
| 
 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
 
wenzelm 
parents: 
47461 
diff
changeset
 | 
118  | 
fi  | 
| 
47115
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
119  | 
}  | 
| 
 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 
wenzelm 
parents: 
46741 
diff
changeset
 | 
120  | 
|
| 
27908
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
121  | 
#CLASSPATH convenience  | 
| 
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
122  | 
function classpath () {
 | 
| 
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
123  | 
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
 | 
124  | 
do  | 
| 
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
125  | 
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
 | 
126  | 
CLASSPATH="$X"  | 
| 
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
127  | 
else  | 
| 
41615
 
f70d2cb26acf
clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;
 
wenzelm 
parents: 
41614 
diff
changeset
 | 
128  | 
CLASSPATH="$X:$CLASSPATH"  | 
| 
27908
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
129  | 
fi  | 
| 
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
130  | 
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
 | 
131  | 
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
 | 
132  | 
}  | 
| 
 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
 
wenzelm 
parents: 
25650 
diff
changeset
 | 
133  | 
|
| 
32390
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
134  | 
#arrays  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
135  | 
function splitarray ()  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
136  | 
{
 | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
137  | 
SPLITARRAY=()  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
138  | 
local IFS="$1"; shift  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
139  | 
for X in $*  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
140  | 
do  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
141  | 
    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
 | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
142  | 
done  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
143  | 
}  | 
| 
 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
 
wenzelm 
parents: 
32321 
diff
changeset
 | 
144  | 
|
| 
32305
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
145  | 
#nested components  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
146  | 
ISABELLE_COMPONENTS=""  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
147  | 
function init_component ()  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
148  | 
{
 | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
149  | 
local COMPONENT="$1"  | 
| 
40570
 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
 
wenzelm 
parents: 
40568 
diff
changeset
 | 
150  | 
case "$COMPONENT" in  | 
| 
 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
 
wenzelm 
parents: 
40568 
diff
changeset
 | 
151  | 
/*) ;;  | 
| 
 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
 
wenzelm 
parents: 
40568 
diff
changeset
 | 
152  | 
*)  | 
| 
 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
 
wenzelm 
parents: 
40568 
diff
changeset
 | 
153  | 
echo >&2 "Absolute component path required: \"$COMPONENT\""  | 
| 
 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
 
wenzelm 
parents: 
40568 
diff
changeset
 | 
154  | 
exit 2  | 
| 
 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
 
wenzelm 
parents: 
40568 
diff
changeset
 | 
155  | 
;;  | 
| 
 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
 
wenzelm 
parents: 
40568 
diff
changeset
 | 
156  | 
esac  | 
| 
32305
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
157  | 
|
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
158  | 
if [ ! -d "$COMPONENT" ]; then  | 
| 41758 | 159  | 
echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""  | 
| 
32305
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
160  | 
exit 2  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
161  | 
elif [ -z "$ISABELLE_COMPONENTS" ]; then  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
162  | 
ISABELLE_COMPONENTS="$COMPONENT"  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
163  | 
else  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
164  | 
ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
165  | 
fi  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
166  | 
if [ -f "$COMPONENT/etc/settings" ]; then  | 
| 
41760
 
bf49b7a85936
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
 
wenzelm 
parents: 
41759 
diff
changeset
 | 
167  | 
source "$COMPONENT/etc/settings"  | 
| 
 
bf49b7a85936
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
 
wenzelm 
parents: 
41759 
diff
changeset
 | 
168  | 
local RC="$?"  | 
| 
 
bf49b7a85936
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
 
wenzelm 
parents: 
41759 
diff
changeset
 | 
169  | 
if [ "$RC" -ne 0 ]; then  | 
| 
 
bf49b7a85936
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
 
wenzelm 
parents: 
41759 
diff
changeset
 | 
170  | 
echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""  | 
| 
 
bf49b7a85936
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
 
wenzelm 
parents: 
41759 
diff
changeset
 | 
171  | 
exit 2  | 
| 
 
bf49b7a85936
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
 
wenzelm 
parents: 
41759 
diff
changeset
 | 
172  | 
fi  | 
| 
32305
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
173  | 
fi  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
174  | 
if [ -f "$COMPONENT/etc/components" ]; then  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
175  | 
    {
 | 
| 
33512
 
771ec7306438
init_component: slightly more robust read (raw input, succeed on non-terminated last line);
 
wenzelm 
parents: 
33295 
diff
changeset
 | 
176  | 
      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
 | 
177  | 
do  | 
| 
32305
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
178  | 
case "$REPLY" in  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
179  | 
\#* | "") ;;  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
180  | 
/*) init_component "$REPLY" ;;  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
181  | 
*) init_component "$COMPONENT/$REPLY" ;;  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
182  | 
esac  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
183  | 
done  | 
| 33295 | 184  | 
} < "$COMPONENT/etc/components"  | 
| 
32305
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
185  | 
fi  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
186  | 
}  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
187  | 
|
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
188  | 
#main components  | 
| 
 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 
wenzelm 
parents: 
31520 
diff
changeset
 | 
189  | 
init_component "$ISABELLE_HOME"  | 
| 
32321
 
13920dbe4547
more uniform handling of ISABELLE_HOME_USER component;
 
wenzelm 
parents: 
32305 
diff
changeset
 | 
190  | 
[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"  | 
| 
2299
 
ed9720047d53
getsettings: bash source script to augment current env.
 
wenzelm 
parents:  
diff
changeset
 | 
191  | 
|
| 21490 | 192  | 
#ML system identifier  | 
| 6413 | 193  | 
if [ -z "$ML_PLATFORM" ]; then  | 
194  | 
ML_IDENTIFIER="$ML_SYSTEM"  | 
|
195  | 
else  | 
|
196  | 
  ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
 | 
|
197  | 
fi  | 
|
| 
21468
 
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
 
wenzelm 
parents: 
16293 
diff
changeset
 | 
198  | 
|
| 6413 | 199  | 
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"  | 
| 3118 | 200  | 
|
| 
2299
 
ed9720047d53
getsettings: bash source script to augment current env.
 
wenzelm 
parents:  
diff
changeset
 | 
201  | 
set +o allexport  | 
| 
7770
 
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
 
wenzelm 
parents: 
6413 
diff
changeset
 | 
202  | 
|
| 
 
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
 
wenzelm 
parents: 
6413 
diff
changeset
 | 
203  | 
fi  |