# HG changeset patch
# User wenzelm
# Date 860001146 -7200
# Node ID 477bfcb022d8dfff349897c6102b7784765527e8
# Parent  bf7b6833e4d7fdaf7426840f4d6de87ef7c1eae9
misc improvements;

diff -r bf7b6833e4d7 -r 477bfcb022d8 build
--- 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