author  wenzelm 
Mon, 04 Jan 2010 21:49:47 +0100  
changeset 34254  14f6df4f473d 
parent 34043  7129fab1fe4f 
child 34255  2dd2547acb41 
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 

15972  14 
export ISABELLE_HOME 
12598  15 
if { echo n "$ISABELLE_HOME"  fgrep " " >/dev/null; } 
16 
then 

17 
echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!" 

18 
echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\"" 

19 
fi 

2736  20 

11553  21 
#key executables 
28499
eff93bc3c14f
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL  old bindings stay for a while (legacy feature);
wenzelm
parents:
28055
diff
changeset

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

23 
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" 
28499
eff93bc3c14f
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL  old bindings stay for a while (legacy feature);
wenzelm
parents:
28055
diff
changeset

24 
#legacy settings 
eff93bc3c14f
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL  old bindings stay for a while (legacy feature);
wenzelm
parents:
28055
diff
changeset

25 
ISABELLE="$ISABELLE_PROCESS" 
eff93bc3c14f
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL  old bindings stay for a while (legacy feature);
wenzelm
parents:
28055
diff
changeset

26 
ISATOOL="$ISABELLE_TOOL" 
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset

27 

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

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

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

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

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

32 

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

33 
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

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

35 
"$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

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

37 

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

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

39 
ISABELLE_IDENTIFIER="" 
21490  40 

2643  41 
#users tend to put strange things in here ... 
2621  42 
unset ENV 
43 
unset BASH_ENV 

44 

9680  45 
#support easy settings 
46 
function choosefrom () 

47 
{ 

48 
local RESULT="" 

49 
local FILE="" 

50 

51 
for FILE in "$@" 

52 
do 

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

54 
done 

55 

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

57 
echo "$RESULT" 

58 
} 

59 

27914  60 
#JVM path wrapper 
25650  61 
if [ "$OSTYPE" = cygwin ]; then 
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset

62 
CLASSPATH="$(cygpath u p "$CLASSPATH")" 
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset

63 
function jvmpath() { cygpath w p "$@"; } 
34043
7129fab1fe4f
more robust Cygwin.config: actually check Wow6432Node, prefer explicit CYGWIN_ROOT in any case;
wenzelm
parents:
33512
diff
changeset

64 
CYGWIN_ROOT="$(jvmpath "/")" 
25650  65 
else 
27908
97f8b7c0f420
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
wenzelm
parents:
25650
diff
changeset

66 
function jvmpath() { echo "$@"; } 
25650  67 
fi 
28055
eb855c3db657
provide HOME_JVM=HOME to prevent implicit cygpath mangling;
wenzelm
parents:
27940
diff
changeset

68 
HOME_JVM="$HOME" 
25650  69 

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

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

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

72 
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

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

74 
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

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

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

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

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

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

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

81 

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

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

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

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

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

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

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

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

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

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

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

92 

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

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

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

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

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

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

98 

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

99 
if [ ! d "$COMPONENT" ]; then 
33295  100 
echo >&2 "Bad Isabelle component: \"$COMPONENT\"" 
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

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

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

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

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

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

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

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

108 
source "$COMPONENT/etc/settings"  exit 2 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

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

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

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

112 
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

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

114 
case "$REPLY" in 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

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

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

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

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

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

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

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

123 

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

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

125 
init_component "$ISABELLE_HOME" 
9789  126 

127 
[ "$ISABELLE_HOME" ef "$ISABELLE_HOME_USER" ] && \ 

32321
13920dbe4547
more uniform handling of ISABELLE_HOME_USER component;
wenzelm
parents:
32305
diff
changeset

128 
{ echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; } 
13920dbe4547
more uniform handling of ISABELLE_HOME_USER component;
wenzelm
parents:
32305
diff
changeset

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

130 

21490  131 
#ML system identifier 
6413  132 
if [ z "$ML_PLATFORM" ]; then 
133 
ML_IDENTIFIER="$ML_SYSTEM" 

134 
else 

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

136 
fi 

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

137 

6413  138 
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" 
3118  139 

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

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

141 

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

142 
fi 