author  wenzelm 
Wed, 17 Feb 2016 23:06:24 +0100  
changeset 62354  fdd6989cc8a0 
parent 61319  d84b4d39bce1 
child 62412  ffdc5cf36dc5 
permissions  rwxrxrx 
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset

1 
# * shellscript * :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 

57411
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script  e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset

19 
#sane environment defaults (notably on Mac OS X) 
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script  e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset

20 
if [ "$ISABELLE_APP" = true a x /usr/libexec/path_helper ]; then 
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script  e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset

21 
eval $(/usr/libexec/path_helper s) 
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script  e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset

22 
fi 
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script  e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset

23 

48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

24 
#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

25 
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

26 
then 
53970  27 
unset INI_DIR 
28 

58640
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within readonly directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents:
58413
diff
changeset

29 
if [ n "$TEMP_WINDOWS" ]; then 
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within readonly directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents:
58413
diff
changeset

30 
TMPDIR="$(cygpath u "$TEMP_WINDOWS")" 
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within readonly directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents:
58413
diff
changeset

31 
TMP="$TMPDIR" 
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within readonly directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents:
58413
diff
changeset

32 
TEMP="$TMPDIR" 
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within readonly directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents:
58413
diff
changeset

33 
fi 
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within readonly directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents:
58413
diff
changeset

34 

47661
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

35 
if [ z "$USER_HOME" ]; then 
60531
9cc91b8a6489
less ambitious USER_HOME on Windows: avoid potentially disconnected share, agree with guess of JVM user.home;
wenzelm
parents:
58791
diff
changeset

36 
USER_HOME="$(cygpath u "$USERPROFILE")" 
47661
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

37 
fi 
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

38 

61294  39 
function platform_path() { cygpath i C UTF8 w p "$@"; } 
40 
CYGWIN_ROOT="$(platform_path "/")" 

41 
ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")" 

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 addon resources);
wenzelm
parents:
52443
diff
changeset

42 

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 addon resources);
wenzelm
parents:
52443
diff
changeset

43 
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 addon resources);
wenzelm
parents:
52443
diff
changeset

44 
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

45 
else 
47661
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

46 
if [ z "$USER_HOME" ]; then 
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

47 
USER_HOME="$HOME" 
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

48 
fi 
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

49 

61293
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents:
61159
diff
changeset

50 
ISABELLE_ROOT="$ISABELLE_HOME" 
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents:
61159
diff
changeset

51 

61294  52 
function platform_path() { 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 addon resources);
wenzelm
parents:
52443
diff
changeset

53 

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 addon resources);
wenzelm
parents:
52443
diff
changeset

54 
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 addon resources);
wenzelm
parents:
52443
diff
changeset

55 
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

56 
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

57 

15972  58 
export ISABELLE_HOME 
2736  59 

11553  60 
#key executables 
56440  61 
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" 
56439
95e2656b3b23
renamed "isabelleprocess" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
53970
diff
changeset

62 
ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process" 
56448
344800503974
provide oldstyle ISABELLE_SCALA_SCRIPT for uniformity;
wenzelm
parents:
56440
diff
changeset

63 
ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script" 
56440  64 

65 
function isabelle () 

66 
{ 

67 
"$ISABELLE_TOOL" "$@" 

68 
} 

2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset

69 

56439
95e2656b3b23
renamed "isabelleprocess" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
53970
diff
changeset

70 
function isabelle_process () 
95e2656b3b23
renamed "isabelleprocess" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
53970
diff
changeset

71 
{ 
95e2656b3b23
renamed "isabelleprocess" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
53970
diff
changeset

72 
"$ISABELLE_PROCESS" "$@" 
95e2656b3b23
renamed "isabelleprocess" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
53970
diff
changeset

73 
} 
95e2656b3b23
renamed "isabelleprocess" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
53970
diff
changeset

74 

56440  75 
function isabelle_scala_script () 
34254
14f6df4f473d
shell functions "isabelleprocess" and "isabelle" refer to the proper executables statically  for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset

76 
{ 
56448
344800503974
provide oldstyle ISABELLE_SCALA_SCRIPT for uniformity;
wenzelm
parents:
56440
diff
changeset

77 
"$ISABELLE_SCALA_SCRIPT" "$@" 
34254
14f6df4f473d
shell functions "isabelleprocess" and "isabelle" refer to the proper executables statically  for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset

78 
} 
14f6df4f473d
shell functions "isabelleprocess" and "isabelle" refer to the proper executables statically  for interactive use or sloppy bash scripts;
wenzelm
parents:
34043
diff
changeset

79 

36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64  NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset

80 
#platform 
41758  81 
source "$ISABELLE_HOME/lib/scripts/isabelleplatform" 
48455  82 
if [ z "$ISABELLE_PLATFORM" ]; then 
83 
echo 1>&2 "Failed to determine hardware and operating system type!" 

84 
exit 2 

85 
fi 

36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64  NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset

86 

25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset

87 
#Isabelle distribution identifier  filled in automatically! 
41511  88 
ISABELLE_ID="" 
48837
d1d806a42c91
allow to provide external ISABELLE_IDENTIFIER for repository clone  potentially relevant for isatest and mira;
wenzelm
parents:
48790
diff
changeset

89 
[ z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="" 
21490  90 

41511  91 
#sometimes users put strange things in here ... 
2621  92 
unset ENV 
93 
unset BASH_ENV 

94 

41614
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

95 
#shared library convenience 
52443  96 
function librarypath () 
97 
{ 

41614
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

98 
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

99 
do 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

100 
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

101 
*darwin) 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

102 
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

103 
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

104 
else 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

105 
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

106 
fi 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

107 
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

108 
;; 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

109 
*) 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

110 
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

111 
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

112 
else 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

113 
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

114 
fi 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

115 
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

116 
;; 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

117 
esac 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

118 
done 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

119 
} 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

120 

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 
#robust invocation via ISABELLE_JDK_HOME 
52443  122 
function isabelle_jdk () 
123 
{ 

47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

124 
if [ z "$ISABELLE_JDK_HOME" ]; then 
58791  125 
echo "Unknown ISABELLE_JDK_HOME  Java development tools unavailable" >&2 
47490
f4348634595b
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents:
47465
diff
changeset

126 
return 127 
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

127 
else 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

128 
local PRG="$1"; shift 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

129 
"$ISABELLE_JDK_HOME/bin/$PRG" "$@" 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

130 
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

131 
} 
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

132 

58791  133 
#robust invocation via JAVA_HOME 
134 
function isabelle_java () 

135 
{ 

136 
if [ z "$JAVA_HOME" ]; then 

137 
echo "Unknown JAVA_HOME  Java unavailable" >&2 

138 
return 127 

139 
else 

140 
local PRG="$1"; shift 

141 
"$JAVA_HOME/bin/$PRG" "$@" 

142 
fi 

143 
} 

144 

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

145 
#robust invocation via SCALA_HOME 
52443  146 
function isabelle_scala () 
147 
{ 

58791  148 
if [ z "$JAVA_HOME" ]; then 
149 
echo "Unknown JAVA_HOME  Java unavailable" >&2 

47490
f4348634595b
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents:
47465
diff
changeset

150 
return 127 
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

151 
elif [ z "$SCALA_HOME" ]; then 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

152 
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

153 
return 127 
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

154 
else 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

155 
local PRG="$1"; shift 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

156 
"$SCALA_HOME/bin/$PRG" "$@" 
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

157 
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

158 
} 
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

159 

52443  160 
#administrative build 
161 
if [ e "$ISABELLE_HOME/Admin/build" ]; then 

162 
function isabelle_admin_build () 

163 
{ 

164 
"$ISABELLE_HOME/Admin/build" "$@" 

165 
} 

166 
else 

167 
function isabelle_admin_build () { return 0; } 

168 
fi 

169 

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 addon resources);
wenzelm
parents:
52443
diff
changeset

170 
#classpath 
52443  171 
function classpath () 
172 
{ 

27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset

173 
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

174 
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 addon resources);
wenzelm
parents:
52443
diff
changeset

175 
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 addon resources);
wenzelm
parents:
52443
diff
changeset

176 
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

177 
else 
53580  178 
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

179 
fi 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset

180 
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 addon resources);
wenzelm
parents:
52443
diff
changeset

181 
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

182 
} 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset

183 

32390
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

184 
#arrays 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

185 
function splitarray () 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

186 
{ 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

187 
SPLITARRAY=() 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

188 
local IFS="$1"; shift 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

189 
for X in $* 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

190 
do 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

191 
SPLITARRAY["${#SPLITARRAY[@]}"]="$X" 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

192 
done 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

193 
} 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

194 

48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

195 

623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

196 
# components 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

197 

32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

198 
ISABELLE_COMPONENTS="" 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

199 
ISABELLE_COMPONENTS_MISSING="" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

200 

623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

201 
#init component tree 
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

202 
function init_component () 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

203 
{ 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

204 
local COMPONENT="$1" 
40570
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset

205 
case "$COMPONENT" in 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset

206 
/*) ;; 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset

207 
*) 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset

208 
echo >&2 "Absolute component path required: \"$COMPONENT\"" 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset

209 
exit 2 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset

210 
;; 
bf8f92bdf630
init_component: require absolute path (when invoked by user scripts);
wenzelm
parents:
40568
diff
changeset

211 
esac 
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

212 

48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

213 
if [ d "$COMPONENT" ]; then 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

214 
if [ z "$ISABELLE_COMPONENTS" ]; then 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

215 
ISABELLE_COMPONENTS="$COMPONENT" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

216 
else 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

217 
ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

218 
fi 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

219 
else 
48448  220 
echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

221 
if [ z "$ISABELLE_COMPONENTS_MISSING" ]; then 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

222 
ISABELLE_COMPONENTS_MISSING="$COMPONENT" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

223 
else 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

224 
ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

225 
fi 
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

226 
fi 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

227 

32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
fi 
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

235 
fi 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

236 
if [ f "$COMPONENT/etc/components" ]; then 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

237 
init_components "$COMPONENT" "$COMPONENT/etc/components" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

238 
fi 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

239 
} 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

240 

623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

241 
#init component forest 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

242 
function init_components () 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

243 
{ 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

244 
local BASE="$1" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

245 
local CATALOG="$2" 
61159
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

246 
local COMPONENT="" 
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

247 
local a COMPONENTS=() 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

248 

623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

249 
if [ ! f "$CATALOG" ]; then 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

250 
echo >&2 "Bad component catalog file: \"$CATALOG\"" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

251 
exit 2 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

252 
fi 
61159
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

253 

48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

254 
{ 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

255 
while { unset REPLY; read r; test "$?" = 0 o n "$REPLY"; } 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

256 
do 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

257 
case "$REPLY" in 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

258 
\#*  "") ;; 
61159
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

259 
/*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;; 
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

260 
*) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;; 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

261 
esac 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

262 
done 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

263 
} < "$CATALOG" 
61159
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

264 

da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

265 
for COMPONENT in "${COMPONENTS[@]}" 
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

266 
do 
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

267 
init_component "$COMPONENT" 
da900891ee06
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
wenzelm
parents:
60531
diff
changeset

268 
done 
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

269 
} 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

270 

c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

271 
#main components 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

272 
init_component "$ISABELLE_HOME" 
48725
e852f4d6af80
configure Admin as component, with its own lib/Tools;
wenzelm
parents:
48551
diff
changeset

273 
[ d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" 
61319
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod w for heap images;
wenzelm
parents:
61294
diff
changeset

274 
if [ d "$ISABELLE_HOME_USER" ]; then 
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod w for heap images;
wenzelm
parents:
61294
diff
changeset

275 
init_component "$ISABELLE_HOME_USER" 
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod w for heap images;
wenzelm
parents:
61294
diff
changeset

276 
else 
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod w for heap images;
wenzelm
parents:
61294
diff
changeset

277 
mkdir p "$ISABELLE_HOME_USER" 
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod w for heap images;
wenzelm
parents:
61294
diff
changeset

278 
chmod $(umask S) "$ISABELLE_HOME_USER" 
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod w for heap images;
wenzelm
parents:
61294
diff
changeset

279 
fi 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

280 

21490  281 
#ML system identifier 
6413  282 
if [ z "$ML_PLATFORM" ]; then 
283 
ML_IDENTIFIER="$ML_SYSTEM" 

284 
else 

285 
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" 

286 
fi 

21468
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents:
16293
diff
changeset

287 

48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

288 
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

289 

47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset

290 
#enforce JAVA_HOME 
58791  291 
export JAVA_HOME="$ISABELLE_JDK_HOME/jre" 
47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset

292 

2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset

293 
set +o allexport 
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset

294 

0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset

295 
fi 