author | wenzelm |
Mon, 11 Nov 2013 17:34:44 +0100 | |
changeset 54383 | 9d3c7a04a65e |
parent 53970 | eee1863c565a |
child 56439 | 95e2656b3b23 |
permissions | -rwxr-xr-x |
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 |
|
53913
5ff12177a067
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm
parents:
53580
diff
changeset
|
14 |
#GNU tar (notably on Mac OS X) |
5ff12177a067
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm
parents:
53580
diff
changeset
|
15 |
if [ -x /usr/bin/gnutar ]; then |
5ff12177a067
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm
parents:
53580
diff
changeset
|
16 |
function tar() { /usr/bin/gnutar "$@"; } |
5ff12177a067
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm
parents:
53580
diff
changeset
|
17 |
fi |
5ff12177a067
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm
parents:
53580
diff
changeset
|
18 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
19 |
#Cygwin vs. POSIX |
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
|
20 |
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
|
21 |
then |
53970 | 22 |
unset INI_DIR |
23 |
||
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
24 |
if [ -z "$USER_HOME" ]; then |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
25 |
USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")" |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
26 |
fi |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
27 |
|
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
|
28 |
function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
47996
25b9f59ab1b9
simplified Cygwin root: warm start via env, cold start via property, no registry magic;
wenzelm
parents:
47748
diff
changeset
|
29 |
CYGWIN_ROOT="$(jvmpath "/")" |
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
30 |
|
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
31 |
ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
32 |
unset CLASSPATH |
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
|
33 |
else |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
34 |
if [ -z "$USER_HOME" ]; then |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
35 |
USER_HOME="$HOME" |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
36 |
fi |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
37 |
|
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
|
38 |
function jvmpath() { echo "$@"; } |
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
39 |
|
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
40 |
ISABELLE_CLASSPATH="$CLASSPATH" |
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
41 |
unset CLASSPATH |
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
|
42 |
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
|
43 |
|
15972 | 44 |
export ISABELLE_HOME |
2736 | 45 |
|
11553 | 46 |
#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
|
47 |
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
|
48 |
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
49 |
|
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
|
50 |
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
|
51 |
{ |
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
|
52 |
"$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
|
53 |
} |
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
|
54 |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
55 |
#platform |
41758 | 56 |
source "$ISABELLE_HOME/lib/scripts/isabelle-platform" |
48455 | 57 |
if [ -z "$ISABELLE_PLATFORM" ]; then |
58 |
echo 1>&2 "Failed to determine hardware and operating system type!" |
|
59 |
exit 2 |
|
60 |
fi |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
61 |
|
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
62 |
#Isabelle distribution identifier -- filled in automatically! |
41511 | 63 |
ISABELLE_ID="" |
48837
d1d806a42c91
allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira;
wenzelm
parents:
48790
diff
changeset
|
64 |
[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="" |
21490 | 65 |
|
41511 | 66 |
#sometimes users put strange things in here ... |
2621 | 67 |
unset ENV |
68 |
unset BASH_ENV |
|
69 |
||
41614
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset
|
70 |
#shared library convenience |
52443 | 71 |
function librarypath () |
72 |
{ |
|
41614
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 |
52443 | 97 |
function isabelle_jdk () |
98 |
{ |
|
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
99 |
if [ -z "$ISABELLE_JDK_HOME" ]; then |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
100 |
echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
47490
f4348634595b
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents:
47465
diff
changeset
|
101 |
return 127 |
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
102 |
else |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
103 |
local PRG="$1"; shift |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
104 |
"$ISABELLE_JDK_HOME/bin/$PRG" "$@" |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
105 |
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
|
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 |
|
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 |
#robust invocation via SCALA_HOME |
52443 | 109 |
function isabelle_scala () |
110 |
{ |
|
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
111 |
if [ -z "$ISABELLE_JDK_HOME" ]; then |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
112 |
echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
47490
f4348634595b
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents:
47465
diff
changeset
|
113 |
return 127 |
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
114 |
elif [ -z "$SCALA_HOME" ]; then |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
115 |
echo "Unknown SCALA_HOME -- Scala unavailable" >&2 |
47490
f4348634595b
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents:
47465
diff
changeset
|
116 |
return 127 |
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
117 |
else |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
118 |
local PRG="$1"; shift |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
119 |
"$SCALA_HOME/bin/$PRG" "$@" |
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset
|
120 |
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
|
121 |
} |
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
|
122 |
|
52443 | 123 |
#administrative build |
124 |
if [ -e "$ISABELLE_HOME/Admin/build" ]; then |
|
125 |
function isabelle_admin_build () |
|
126 |
{ |
|
127 |
"$ISABELLE_HOME/Admin/build" "$@" |
|
128 |
} |
|
129 |
else |
|
130 |
function isabelle_admin_build () { return 0; } |
|
131 |
fi |
|
132 |
||
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
133 |
#classpath |
52443 | 134 |
function classpath () |
135 |
{ |
|
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
136 |
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
|
137 |
do |
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
138 |
if [ -z "$ISABELLE_CLASSPATH" ]; then |
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
139 |
ISABELLE_CLASSPATH="$X" |
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
140 |
else |
53580 | 141 |
ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" |
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
142 |
fi |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
143 |
done |
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
144 |
export ISABELLE_CLASSPATH |
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
145 |
} |
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset
|
146 |
|
32390
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
147 |
#arrays |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
148 |
function splitarray () |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
149 |
{ |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
150 |
SPLITARRAY=() |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
151 |
local IFS="$1"; shift |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
152 |
for X in $* |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
153 |
do |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
154 |
SPLITARRAY["${#SPLITARRAY[@]}"]="$X" |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
155 |
done |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
156 |
} |
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset
|
157 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
158 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
159 |
# components |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
160 |
|
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
161 |
ISABELLE_COMPONENTS="" |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
162 |
ISABELLE_COMPONENTS_MISSING="" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
163 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
164 |
#init component tree |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
165 |
function init_component () |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
166 |
{ |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
167 |
local COMPONENT="$1" |
40570
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
168 |
case "$COMPONENT" in |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
169 |
/*) ;; |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
170 |
*) |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
171 |
echo >&2 "Absolute component path required: \"$COMPONENT\"" |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
172 |
exit 2 |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
173 |
;; |
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset
|
174 |
esac |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
175 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
176 |
if [ -d "$COMPONENT" ]; then |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
177 |
if [ -z "$ISABELLE_COMPONENTS" ]; then |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
178 |
ISABELLE_COMPONENTS="$COMPONENT" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
179 |
else |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
180 |
ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
181 |
fi |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
182 |
else |
48448 | 183 |
echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
184 |
if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
185 |
ISABELLE_COMPONENTS_MISSING="$COMPONENT" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
186 |
else |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
187 |
ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
188 |
fi |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
189 |
fi |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
190 |
|
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
191 |
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
|
192 |
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
|
193 |
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
|
194 |
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
|
195 |
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
|
196 |
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
|
197 |
fi |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
198 |
fi |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
199 |
if [ -f "$COMPONENT/etc/components" ]; then |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
200 |
init_components "$COMPONENT" "$COMPONENT/etc/components" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
201 |
fi |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
202 |
} |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
203 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
204 |
#init component forest |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
205 |
function init_components () |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
206 |
{ |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
207 |
local BASE="$1" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
208 |
local CATALOG="$2" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
209 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
210 |
if [ ! -f "$CATALOG" ]; then |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
211 |
echo >&2 "Bad component catalog file: \"$CATALOG\"" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
212 |
exit 2 |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
213 |
fi |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
214 |
{ |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
215 |
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
216 |
do |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
217 |
case "$REPLY" in |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
218 |
\#* | "") ;; |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
219 |
/*) init_component "$REPLY" ;; |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
220 |
*) init_component "$BASE/$REPLY" ;; |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
221 |
esac |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
222 |
done |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
223 |
} < "$CATALOG" |
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
224 |
} |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
225 |
|
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
226 |
#main components |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
227 |
init_component "$ISABELLE_HOME" |
48725
e852f4d6af80
configure Admin as component, with its own lib/Tools;
wenzelm
parents:
48551
diff
changeset
|
228 |
[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" |
32321
13920dbe4547
more uniform handling of ISABELLE_HOME_USER component;
wenzelm
parents:
32305
diff
changeset
|
229 |
[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
230 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
231 |
|
21490 | 232 |
#ML system identifier |
6413 | 233 |
if [ -z "$ML_PLATFORM" ]; then |
234 |
ML_IDENTIFIER="$ML_SYSTEM" |
|
235 |
else |
|
236 |
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
|
237 |
fi |
|
21468
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents:
16293
diff
changeset
|
238 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
239 |
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
240 |
|
47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset
|
241 |
#enforce JAVA_HOME |
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset
|
242 |
export JAVA_HOME="$ISABELLE_JDK_HOME" |
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset
|
243 |
|
48495 | 244 |
#build condition etc. |
245 |
case "$ML_SYSTEM" in |
|
246 |
polyml*) |
|
247 |
ISABELLE_POLYML="true" |
|
248 |
;; |
|
249 |
*) |
|
250 |
ISABELLE_POLYML="" |
|
251 |
;; |
|
252 |
esac |
|
253 |
||
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
254 |
set +o allexport |
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
255 |
|
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
256 |
fi |