159 echo >&2 "Absolute component path required: \"$COMPONENT\"" |
164 echo >&2 "Absolute component path required: \"$COMPONENT\"" |
160 exit 2 |
165 exit 2 |
161 ;; |
166 ;; |
162 esac |
167 esac |
163 |
168 |
164 if [ ! -d "$COMPONENT" ]; then |
169 if [ -d "$COMPONENT" ]; then |
|
170 if [ -z "$ISABELLE_COMPONENTS" ]; then |
|
171 ISABELLE_COMPONENTS="$COMPONENT" |
|
172 else |
|
173 ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
|
174 fi |
|
175 else |
165 echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" |
176 echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" |
166 elif [ -z "$ISABELLE_COMPONENTS" ]; then |
177 if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then |
167 ISABELLE_COMPONENTS="$COMPONENT" |
178 ISABELLE_COMPONENTS_MISSING="$COMPONENT" |
168 else |
179 else |
169 ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" |
180 ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" |
170 fi |
181 fi |
|
182 fi |
|
183 |
171 if [ -f "$COMPONENT/etc/settings" ]; then |
184 if [ -f "$COMPONENT/etc/settings" ]; then |
172 source "$COMPONENT/etc/settings" |
185 source "$COMPONENT/etc/settings" |
173 local RC="$?" |
186 local RC="$?" |
174 if [ "$RC" -ne 0 ]; then |
187 if [ "$RC" -ne 0 ]; then |
175 echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" |
188 echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" |
176 exit 2 |
189 exit 2 |
177 fi |
190 fi |
178 fi |
191 fi |
179 if [ -f "$COMPONENT/etc/components" ]; then |
192 if [ -f "$COMPONENT/etc/components" ]; then |
180 { |
193 init_components "$COMPONENT" "$COMPONENT/etc/components" |
181 while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } |
194 fi |
182 do |
195 } |
183 case "$REPLY" in |
196 |
184 \#* | "") ;; |
197 #init component forest |
185 /*) init_component "$REPLY" ;; |
198 function init_components () |
186 *) init_component "$COMPONENT/$REPLY" ;; |
199 { |
187 esac |
200 local BASE="$1" |
188 done |
201 local CATALOG="$2" |
189 } < "$COMPONENT/etc/components" |
202 |
190 fi |
203 if [ ! -d "$BASE" ]; then |
|
204 echo >&2 "Bad component base directory: \"$BASE\"" |
|
205 exit 2 |
|
206 fi |
|
207 if [ ! -f "$CATALOG" ]; then |
|
208 echo >&2 "Bad component catalog file: \"$CATALOG\"" |
|
209 exit 2 |
|
210 fi |
|
211 { |
|
212 while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } |
|
213 do |
|
214 case "$REPLY" in |
|
215 \#* | "") ;; |
|
216 /*) init_component "$REPLY" ;; |
|
217 *) init_component "$BASE/$REPLY" ;; |
|
218 esac |
|
219 done |
|
220 } < "$CATALOG" |
191 } |
221 } |
192 |
222 |
193 #main components |
223 #main components |
194 init_component "$ISABELLE_HOME" |
224 init_component "$ISABELLE_HOME" |
195 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" |
225 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" |
196 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
226 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
|
227 |
197 |
228 |
198 #ML system identifier |
229 #ML system identifier |
199 if [ -z "$ML_PLATFORM" ]; then |
230 if [ -z "$ML_PLATFORM" ]; then |
200 ML_IDENTIFIER="$ML_SYSTEM" |
231 ML_IDENTIFIER="$ML_SYSTEM" |
201 else |
232 else |
202 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
233 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
203 fi |
234 fi |
204 |
235 |
|
236 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
|
237 |
205 #enforce JAVA_HOME |
238 #enforce JAVA_HOME |
206 export JAVA_HOME="$ISABELLE_JDK_HOME" |
239 export JAVA_HOME="$ISABELLE_JDK_HOME" |
207 |
|
208 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
|
209 |
240 |
210 #build condition etc. |
241 #build condition etc. |
211 case "$ML_SYSTEM" in |
242 case "$ML_SYSTEM" in |
212 polyml*) |
243 polyml*) |
213 ISABELLE_POLYML="true" |
244 ISABELLE_POLYML="true" |