author  wenzelm 
Sun, 22 Apr 2012 14:30:18 +0200  
changeset 47661  012a887997f3 
parent 47525  9c8a1b9c0630 
child 47748  24550210de0b 
permissions  rwrr 
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 

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

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

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 
47661
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

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

18 
USER_HOME="$(cygpath u "$HOMEDRIVE\\$HOMEPATH")" 
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

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

20 

47525
9c8a1b9c0630
retain ISABELLE_HOME_WINDOWS which is useful for jEdit to fold file names symbolically, but without DOS expansion that causes problems with Cygwin/Posix roundtrip (cf. 5a7903ba2dac);
wenzelm
parents:
47490
diff
changeset

21 
ISABELLE_HOME_WINDOWS="$(cygpath w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")" 
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

22 
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

23 

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

25 
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

26 
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

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

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

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

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

31 

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

32 
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

33 
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

34 
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

35 

15972  36 
export ISABELLE_HOME 
12598  37 
if { echo n "$ISABELLE_HOME"  fgrep " " >/dev/null; } 
38 
then 

45094
a43694a0b726
tuned message, which is displayed after termination of Isabelle.app on Mac OS;
wenzelm
parents:
43519
diff
changeset

39 
echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!" 
12598  40 
echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\"" 
41 
fi 

2736  42 

11553  43 
#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

44 
ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelleprocess" 
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelleprocess), renamed isatool to isabelle;
wenzelm
parents:
28499
diff
changeset

45 
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" 
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset

46 

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

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

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

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

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

51 

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

52 
#platform 
41758  53 
source "$ISABELLE_HOME/lib/scripts/isabelleplatform" 
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64  NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset

54 

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

55 
#Isabelle distribution identifier  filled in automatically! 
41511  56 
ISABELLE_ID="" 
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset

57 
ISABELLE_IDENTIFIER="" 
21490  58 

41511  59 
#sometimes users put strange things in here ... 
2621  60 
unset ENV 
61 
unset BASH_ENV 

62 

9680  63 
#support easy settings 
64 
function choosefrom () 

65 
{ 

66 
local RESULT="" 

67 
local FILE="" 

68 

69 
for FILE in "$@" 

70 
do 

71 
[ z "$RESULT" a e "$FILE" ] && RESULT="$FILE" 

72 
done 

73 

74 
[ z "$RESULT" ] && RESULT="$FILE" 

75 
echo "$RESULT" 

76 
} 

77 

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

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

79 
function librarypath () { 
b7cd80330a16
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm
parents:
41511
diff
changeset

80 
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

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

82 
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

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

84 
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

85 
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

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

87 
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

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

89 
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

90 
;; 
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 
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

93 
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

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

95 
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

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

97 
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

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

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

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

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

102 

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

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

104 
function isabelle_jdk () { 
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

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

106 
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

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

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

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

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

111 
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

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

113 

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

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

115 
function isabelle_scala () { 
47465
71d5f37ee2bf
more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;
wenzelm
parents:
47461
diff
changeset

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

117 
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

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

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

120 
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

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

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

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

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

125 
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

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

127 

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

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

129 
function classpath () { 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset

130 
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

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

132 
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

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

134 
else 
41615
f70d2cb26acf
clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;
wenzelm
parents:
41614
diff
changeset

135 
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

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

137 
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

138 
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

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

140 

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

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

142 
function splitarray () 
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 
SPLITARRAY=() 
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32321
diff
changeset

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

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

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

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

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

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

151 

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

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

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

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

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

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

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

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

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

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

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

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

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

164 

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

165 
if [ ! d "$COMPONENT" ]; then 
41758  166 
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

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

168 
elif [ z "$ISABELLE_COMPONENTS" ]; then 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

169 
ISABELLE_COMPONENTS="$COMPONENT" 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

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

171 
ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

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

173 
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

174 
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

175 
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

176 
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

177 
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

178 
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

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

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

181 
if [ f "$COMPONENT/etc/components" ]; then 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

182 
{ 
33512
771ec7306438
init_component: slightly more robust read (raw input, succeed on nonterminated last line);
wenzelm
parents:
33295
diff
changeset

183 
while { unset REPLY; read r; test "$?" = 0 o n "$REPLY"; } 
771ec7306438
init_component: slightly more robust read (raw input, succeed on nonterminated last line);
wenzelm
parents:
33295
diff
changeset

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

185 
case "$REPLY" in 
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 
/*) init_component "$REPLY" ;; 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

188 
*) init_component "$COMPONENT/$REPLY" ;; 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

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

190 
done 
33295  191 
} < "$COMPONENT/etc/components" 
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

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

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

194 

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

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

196 
init_component "$ISABELLE_HOME" 
32321
13920dbe4547
more uniform handling of ISABELLE_HOME_USER component;
wenzelm
parents:
32305
diff
changeset

197 
[ d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" 
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset

198 

21490  199 
#ML system identifier 
6413  200 
if [ z "$ML_PLATFORM" ]; then 
201 
ML_IDENTIFIER="$ML_SYSTEM" 

202 
else 

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

204 
fi 

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

205 

6413  206 
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" 
3118  207 

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

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

209 

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

210 
fi 