author | wenzelm |
Tue, 11 May 2021 20:19:07 +0200 | |
changeset 73675 | 6c56f2ebe157 |
parent 73580 | a96564139fa7 |
child 73773 | ac7f41b66e1b |
permissions | -rw-r--r-- |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
1 |
# -*- shell-script -*- :mode=shellscript: |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
2 |
# |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
3 |
# Author: Makarius |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
4 |
# |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
5 |
# Isabelle shell functions, with on-demand re-initialization for |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
6 |
# non-interactive bash processess. NB: bash shell functions are not portable |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
7 |
# and may be dropped by aggressively POSIX-conformant versions of /bin/sh. |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
8 |
|
62416 | 9 |
if type splitarray >/dev/null 2>/dev/null |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
10 |
then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
11 |
: |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
12 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
13 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
14 |
if [ "$OSTYPE" = cygwin ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
15 |
function platform_path() { cygpath -i -C UTF8 -w -p "$@"; } |
69157 | 16 |
function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; } |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
17 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
18 |
function platform_path() { echo "$@"; } |
69157 | 19 |
function standard_path() { echo "$@"; } |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
20 |
fi |
69157 | 21 |
export -f platform_path standard_path |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
22 |
|
72894
bd2269b6cd99
updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents:
72465
diff
changeset
|
23 |
#GNU tar (notably on macOS) |
73580 | 24 |
function tar() { |
25 |
if [ -f "$ISABELLE_TAR" ]; then |
|
26 |
"$ISABELLE_TAR" "$@" |
|
27 |
else |
|
28 |
"$(type -P tar)" "$@" |
|
29 |
fi |
|
30 |
} |
|
73579 | 31 |
export -f tar |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
32 |
|
69134 | 33 |
#OCaml management via OPAM |
73500 | 34 |
function isabelle_opam () |
69134 | 35 |
{ |
36 |
if [ -z "$ISABELLE_OPAM" ]; then |
|
37 |
echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2 |
|
38 |
return 127 |
|
39 |
else |
|
72465 | 40 |
env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@" |
69134 | 41 |
fi |
42 |
} |
|
43 |
export -f isabelle_opam |
|
44 |
||
69150 | 45 |
#GHC management via Stack |
73500 | 46 |
function isabelle_stack () |
69147 | 47 |
{ |
48 |
if [ -z "$ISABELLE_STACK" ]; then |
|
69150 | 49 |
echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2 |
69147 | 50 |
return 127 |
51 |
else |
|
69267
517655a528fe
always insist in specified resolver/compiler version;
wenzelm
parents:
69255
diff
changeset
|
52 |
env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@" |
69147 | 53 |
fi |
54 |
} |
|
55 |
export -f isabelle_stack |
|
56 |
||
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
57 |
#robust invocation via ISABELLE_JDK_HOME |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
58 |
function isabelle_jdk () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
59 |
{ |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
60 |
if [ -z "$ISABELLE_JDK_HOME" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
61 |
echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
62 |
return 127 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
63 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
64 |
local PRG="$1"; shift |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
65 |
"$ISABELLE_JDK_HOME/bin/$PRG" "$@" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
66 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
67 |
} |
62413 | 68 |
export -f isabelle_jdk |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
69 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
70 |
#robust invocation via JAVA_HOME |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
71 |
function isabelle_java () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
72 |
{ |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
73 |
if [ -z "$JAVA_HOME" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
74 |
echo "Unknown JAVA_HOME -- Java unavailable" >&2 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
75 |
return 127 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
76 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
77 |
local PRG="$1"; shift |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
78 |
"$JAVA_HOME/bin/$PRG" "$@" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
79 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
80 |
} |
62413 | 81 |
export -f isabelle_java |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
82 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
83 |
#robust invocation via SCALA_HOME |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
84 |
function isabelle_scala () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
85 |
{ |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
86 |
if [ -z "$JAVA_HOME" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
87 |
echo "Unknown JAVA_HOME -- Java unavailable" >&2 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
88 |
return 127 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
89 |
elif [ -z "$SCALA_HOME" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
90 |
echo "Unknown SCALA_HOME -- Scala unavailable" >&2 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
91 |
return 127 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
92 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
93 |
local PRG="$1"; shift |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
94 |
"$SCALA_HOME/bin/$PRG" "$@" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
95 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
96 |
} |
62413 | 97 |
export -f isabelle_scala |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
98 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
99 |
#classpath |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
100 |
function classpath () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
101 |
{ |
66667
2e580fcf6522
avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents:
63994
diff
changeset
|
102 |
local X="" |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
103 |
for X in "$@" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
104 |
do |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
105 |
if [ -z "$ISABELLE_CLASSPATH" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
106 |
ISABELLE_CLASSPATH="$X" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
107 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
108 |
ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
109 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
110 |
done |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
111 |
export ISABELLE_CLASSPATH |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
112 |
} |
62413 | 113 |
export -f classpath |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
114 |
|
73513
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
115 |
#java_library |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
116 |
function java_library () |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
117 |
{ |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
118 |
local X="" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
119 |
for X in "$@" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
120 |
do |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
121 |
case "$ISABELLE_PLATFORM_FAMILY" in |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
122 |
linux) |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
123 |
if [ -z "$LD_LIBRARY_PATH" ]; then |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
124 |
export LD_LIBRARY_PATH="$X" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
125 |
else |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
126 |
export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$X" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
127 |
fi |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
128 |
;; |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
129 |
macos) |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
130 |
if [ -z "$JAVA_LIBRARY_PATH" ]; then |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
131 |
export JAVA_LIBRARY_PATH="$X" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
132 |
else |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
133 |
export JAVA_LIBRARY_PATH="$JAVA_LIBRARY_PATH:$X" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
134 |
fi |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
135 |
;; |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
136 |
windows) |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
137 |
if [ -z "$PATH" ]; then |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
138 |
export PATH="$X" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
139 |
else |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
140 |
export PATH="$PATH:$X" |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
141 |
fi |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
142 |
;; |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
143 |
esac |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
144 |
done |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
145 |
export ISABELLE_CLASSPATH |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
146 |
} |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
147 |
export -f java_library |
b7bb665fe850
more systematic java_library: avoid empty entries, declaration order as for other bash functions;
wenzelm
parents:
73500
diff
changeset
|
148 |
|
69342 | 149 |
#Isabelle fonts |
150 |
function isabelle_fonts () |
|
151 |
{ |
|
152 |
local X="" |
|
153 |
for X in "$@" |
|
154 |
do |
|
155 |
if [ -z "$ISABELLE_FONTS" ]; then |
|
156 |
ISABELLE_FONTS="$X" |
|
157 |
else |
|
158 |
ISABELLE_FONTS="$ISABELLE_FONTS:$X" |
|
159 |
fi |
|
160 |
done |
|
161 |
export ISABELLE_FONTS |
|
162 |
} |
|
163 |
export -f isabelle_fonts |
|
164 |
||
69374 | 165 |
function isabelle_fonts_hidden () |
166 |
{ |
|
167 |
local X="" |
|
168 |
for X in "$@" |
|
169 |
do |
|
170 |
if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then |
|
171 |
ISABELLE_FONTS_HIDDEN="$X" |
|
172 |
else |
|
173 |
ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X" |
|
174 |
fi |
|
175 |
done |
|
176 |
export ISABELLE_FONTS_HIDDEN |
|
177 |
} |
|
178 |
export -f isabelle_fonts_hidden |
|
179 |
||
71733 | 180 |
#Isabelle/Scala services |
181 |
function isabelle_scala_service () |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
182 |
{ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
183 |
local X="" |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
184 |
for X in "$@" |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
185 |
do |
71733 | 186 |
if [ -z "$ISABELLE_SCALA_SERVICES" ]; then |
187 |
ISABELLE_SCALA_SERVICES="$X" |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
188 |
else |
71733 | 189 |
ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X" |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
190 |
fi |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
191 |
done |
71733 | 192 |
export ISABELLE_SCALA_SERVICES |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
193 |
} |
71733 | 194 |
export -f isabelle_scala_service |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69157
diff
changeset
|
195 |
|
72162 | 196 |
#Special directories |
197 |
function isabelle_directory () |
|
198 |
{ |
|
199 |
local X="" |
|
200 |
for X in "$@" |
|
201 |
do |
|
202 |
if [ -z "$ISABELLE_DIRECTORIES" ]; then |
|
203 |
ISABELLE_DIRECTORIES="$X" |
|
204 |
else |
|
205 |
ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X" |
|
206 |
fi |
|
207 |
done |
|
208 |
export ISABELLE_DIRECTORIES |
|
209 |
} |
|
210 |
export -f isabelle_directory |
|
211 |
||
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
212 |
#administrative build |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
213 |
if [ -e "$ISABELLE_HOME/Admin/build" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
214 |
function isabelle_admin_build () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
215 |
{ |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
216 |
"$ISABELLE_HOME/Admin/build" "$@" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
217 |
} |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
218 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
219 |
function isabelle_admin_build () { return 0; } |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
220 |
fi |
62413 | 221 |
export -f isabelle_admin_build |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
222 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
223 |
#arrays |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
224 |
function splitarray () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
225 |
{ |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
226 |
SPLITARRAY=() |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
227 |
local IFS="$1"; shift |
66667
2e580fcf6522
avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents:
63994
diff
changeset
|
228 |
local X="" |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
229 |
for X in $* |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
230 |
do |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
231 |
SPLITARRAY["${#SPLITARRAY[@]}"]="$X" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
232 |
done |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
233 |
} |
62413 | 234 |
export -f splitarray |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
235 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
236 |
#init component tree |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
237 |
function init_component () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
238 |
{ |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
239 |
local COMPONENT="$1" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
240 |
case "$COMPONENT" in |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
241 |
/*) ;; |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
242 |
*) |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
243 |
echo >&2 "Absolute component path required: \"$COMPONENT\"" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
244 |
exit 2 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
245 |
;; |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
246 |
esac |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
247 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
248 |
if [ -d "$COMPONENT" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
249 |
if [ -z "$ISABELLE_COMPONENTS" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
250 |
ISABELLE_COMPONENTS="$COMPONENT" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
251 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
252 |
ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
253 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
254 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
255 |
echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
256 |
if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
257 |
ISABELLE_COMPONENTS_MISSING="$COMPONENT" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
258 |
else |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
259 |
ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
260 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
261 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
262 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
263 |
if [ -f "$COMPONENT/etc/settings" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
264 |
source "$COMPONENT/etc/settings" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
265 |
local RC="$?" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
266 |
if [ "$RC" -ne 0 ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
267 |
echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
268 |
exit 2 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
269 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
270 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
271 |
if [ -f "$COMPONENT/etc/components" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
272 |
init_components "$COMPONENT" "$COMPONENT/etc/components" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
273 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
274 |
} |
62413 | 275 |
export -f init_component |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
276 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
277 |
#init component forest |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
278 |
function init_components () |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
279 |
{ |
66667
2e580fcf6522
avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);
wenzelm
parents:
63994
diff
changeset
|
280 |
local REPLY="" |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
281 |
local BASE="$1" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
282 |
local CATALOG="$2" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
283 |
local COMPONENT="" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
284 |
local -a COMPONENTS=() |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
285 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
286 |
if [ ! -f "$CATALOG" ]; then |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
287 |
echo >&2 "Bad component catalog file: \"$CATALOG\"" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
288 |
exit 2 |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
289 |
fi |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
290 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
291 |
{ |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
292 |
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
293 |
do |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
294 |
case "$REPLY" in |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
295 |
\#* | "") ;; |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
296 |
/*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;; |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
297 |
*) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;; |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
298 |
esac |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
299 |
done |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
300 |
} < "$CATALOG" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
301 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
302 |
for COMPONENT in "${COMPONENTS[@]}" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
303 |
do |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
304 |
init_component "$COMPONENT" |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
305 |
done |
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
306 |
} |
62413 | 307 |
export -f init_components |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
308 |
|
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
diff
changeset
|
309 |
fi |