--- a/build Wed Apr 02 17:28:27 1997 +0200
+++ b/build Wed Apr 02 19:12:26 1997 +0200
@@ -4,10 +4,6 @@
#
# build - compile parts of the Isabelle system
-## args
-
-LOGICS="$*"
-
## settings
@@ -18,33 +14,112 @@
{ echo "$PRG probably not called from its original place!"; exit 2 }
-## tell the user about current values
+## diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
+ echo
+ echo " Options are:"
+ echo " -a all logics"
+ echo
+ echo " Compile the named LOGICS (default $DEFAULT_LOGIC), or all object logics"
+ echo " in the distribution."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+ALL=""
+while getopts "a" OPT
+do
+ case "$OPT" in
+ a)
+ ALL=true
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+LOGICS="$@"
+
+
+## main
+
+# tell the user about current values
+
+echo
+echo " *****************************"
+echo " * Welcome to Isabelle build *"
+echo " *****************************"
echo
echo "Please check $ISABELLE_HOME/etc/settings"
[ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
echo "to make sure that Isabelle's ML system settings are appropriate."
+echo
echo "Your current values are:"
echo
-echo "ML_SYSTEM=$ML_SYSTEM"
-echo "ML_HOME=$ML_HOME"
-echo "ML_OPTIONS=$ML_OPTIONS"
+echo " ML_SYSTEM=$ML_SYSTEM"
+echo " ML_HOME=$ML_HOME"
+echo " ML_OPTIONS=$ML_OPTIONS"
-## build it
-
-LOGICS="Pure $DEFAULT_LOGIC $LOGICS"
+# check logics
echo
echo
-echo "Press RETURN to start compilation of: $LOGICS"
+echo "Press RETURN to start compilation (including parents) of:"
+echo
+
+[ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC
+
+if [ -n "$ALL" ]; then
+ LOGICS=""
+ for DIR in $ISABELLE_HOME/src/*
+ do
+ if [ -f $DIR/IsaMakefile ]; then
+ L=$(basename $DIR)
+ LOGICS="$LOGICS $L"
+ fi
+ done
+else
+ for L in $LOGICS
+ do
+ DIR=$ISABELLE_HOME/src/$L
+ [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
+ done
+fi
+
+echo " " $LOGICS
+echo
read
+# build it
+
export THIS_IS_ISABELLE_BUILD=true
-for DIR in $LOGICS
+for L in $LOGICS
do
- ( cd $ISABELLE_HOME/src/$DIR; $ISATOOL make)
+ ( cd $ISABELLE_HOME/src/$L; $ISATOOL make )
done