1.1 --- a/build	Wed Apr 02 17:28:27 1997 +0200
     1.2 +++ b/build	Wed Apr 02 19:12:26 1997 +0200
     1.3 @@ -4,10 +4,6 @@
     1.4  #
     1.5  # build - compile parts of the Isabelle system
     1.6  
     1.7 -## args
     1.8 -
     1.9 -LOGICS="$*"
    1.10 -
    1.11  
    1.12  ## settings
    1.13  
    1.14 @@ -18,33 +14,112 @@
    1.15    { echo "$PRG probably not called from its original place!"; exit 2 }
    1.16  
    1.17  
    1.18 -## tell the user about current values
    1.19 +## diagnostics
    1.20  
    1.21 +function usage()
    1.22 +{
    1.23 +  echo
    1.24 +  echo "Usage: $PRG [OPTIONS] [LOGICS ...]"
    1.25 +  echo
    1.26 +  echo "  Options are:"
    1.27 +  echo "    -a           all logics"
    1.28 +  echo
    1.29 +  echo "  Compile the named LOGICS (default $DEFAULT_LOGIC), or all object logics"
    1.30 +  echo "  in the distribution."
    1.31 +  echo
    1.32 +  exit 1
    1.33 +}
    1.34 +
    1.35 +function fail()
    1.36 +{
    1.37 +  echo "$1" >&2
    1.38 +  exit 2
    1.39 +}
    1.40 +
    1.41 +
    1.42 +## process command line
    1.43 +
    1.44 +# options
    1.45 +
    1.46 +ALL=""
    1.47 +
    1.48 +while getopts "a" OPT
    1.49 +do
    1.50 +  case "$OPT" in
    1.51 +    a)
    1.52 +      ALL=true
    1.53 +      ;;
    1.54 +    \?)
    1.55 +      usage
    1.56 +      ;;
    1.57 +  esac
    1.58 +done
    1.59 +
    1.60 +shift $(($OPTIND - 1))
    1.61 +
    1.62 +
    1.63 +# args
    1.64 +
    1.65 +LOGICS="$@"
    1.66 +
    1.67 +
    1.68 +## main
    1.69 +
    1.70 +# tell the user about current values
    1.71 +
    1.72 +echo
    1.73 +echo "                *****************************"
    1.74 +echo "                * Welcome to Isabelle build *"
    1.75 +echo "                *****************************"
    1.76  echo
    1.77  echo "Please check $ISABELLE_HOME/etc/settings"
    1.78  [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
    1.79  echo "to make sure that Isabelle's ML system settings are appropriate."
    1.80 +echo
    1.81  echo "Your current values are:"
    1.82  echo
    1.83  
    1.84 -echo "ML_SYSTEM=$ML_SYSTEM"
    1.85 -echo "ML_HOME=$ML_HOME"
    1.86 -echo "ML_OPTIONS=$ML_OPTIONS"
    1.87 +echo "  ML_SYSTEM=$ML_SYSTEM"
    1.88 +echo "  ML_HOME=$ML_HOME"
    1.89 +echo "  ML_OPTIONS=$ML_OPTIONS"
    1.90  
    1.91  
    1.92 -## build it
    1.93 -
    1.94 -LOGICS="Pure $DEFAULT_LOGIC $LOGICS"
    1.95 +# check logics
    1.96  
    1.97  echo
    1.98  echo
    1.99 -echo "Press RETURN to start compilation of: $LOGICS"
   1.100 +echo "Press RETURN to start compilation (including parents) of:"
   1.101 +echo
   1.102 +
   1.103 +[ -z "$LOGICS" ] && LOGICS=$DEFAULT_LOGIC
   1.104 +
   1.105 +if [ -n "$ALL" ]; then
   1.106 +  LOGICS=""
   1.107 +  for DIR in $ISABELLE_HOME/src/*
   1.108 +  do
   1.109 +    if [ -f $DIR/IsaMakefile ]; then
   1.110 +      L=$(basename $DIR)
   1.111 +      LOGICS="$LOGICS $L"
   1.112 +    fi
   1.113 +  done
   1.114 +else
   1.115 +  for L in $LOGICS
   1.116 +  do
   1.117 +    DIR=$ISABELLE_HOME/src/$L
   1.118 +    [ ! -f $DIR/IsaMakefile ] && fail "No such logic: $L"
   1.119 +  done
   1.120 +fi
   1.121 +
   1.122 +echo " " $LOGICS
   1.123 +echo
   1.124  read
   1.125  
   1.126  
   1.127 +# build it
   1.128 +
   1.129  export THIS_IS_ISABELLE_BUILD=true
   1.130  
   1.131 -for DIR in $LOGICS
   1.132 +for L in $LOGICS
   1.133  do
   1.134 -  ( cd $ISABELLE_HOME/src/$DIR; $ISATOOL make)
   1.135 +  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make )
   1.136  done