RAW target;
authorwenzelm
Mon Oct 06 18:20:15 1997 +0200 (1997-10-06)
changeset 3774b1bfd394b60a
parent 3773 989ef5e9d543
child 3775 a99fdf465dfb
RAW target;
src/Pure/IsaMakefile
src/Pure/mk
     1.1 --- a/src/Pure/IsaMakefile	Mon Oct 06 09:26:00 1997 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Oct 06 18:20:15 1997 +0200
     1.3 @@ -21,9 +21,12 @@
     1.4  	search.ML section_utils.ML sequence.ML sign.ML sorts.ML symtab.ML tactic.ML \
     1.5  	tctical.ML term.ML theory.ML thm.ML type.ML type_infer.ML unify.ML
     1.6  
     1.7 -$(OUT)/Pure: $(FILES)
     1.8 +Pure: $(FILES)
     1.9  	@./mk
    1.10  
    1.11 -test: $(OUT)/Pure
    1.12 +RAW: $(FILES)
    1.13 +	@./mk -r
    1.14 +
    1.15 +test: Pure
    1.16  
    1.17  .PRECIOUS: $(OUT)/Pure
     2.1 --- a/src/Pure/mk	Mon Oct 06 09:26:00 1997 +0200
     2.2 +++ b/src/Pure/mk	Mon Oct 06 18:20:15 1997 +0200
     2.3 @@ -9,6 +9,18 @@
     2.4  
     2.5  ## diagnostics
     2.6  
     2.7 +function usage()
     2.8 +{
     2.9 +  echo
    2.10 +  echo "Usage: $PRG [OPTIONS]"
    2.11 +  echo
    2.12 +  echo "  Make Pure Isabelle."
    2.13 +  echo
    2.14 +  echo "    -r           just prepare RAW image"
    2.15 +  echo
    2.16 +  exit 1
    2.17 +}
    2.18 +
    2.19  function fail()
    2.20  {
    2.21    echo "$1" >&2
    2.22 @@ -16,6 +28,32 @@
    2.23  }
    2.24  
    2.25  
    2.26 +## process command line
    2.27 +
    2.28 +# options
    2.29 +
    2.30 +RAW=""
    2.31 +
    2.32 +while getopts "r" OPT
    2.33 +do
    2.34 +  case "$OPT" in
    2.35 +    r)
    2.36 +      RAW=true
    2.37 +      ;;
    2.38 +    \?)
    2.39 +      usage
    2.40 +      ;;
    2.41 +  esac
    2.42 +done
    2.43 +
    2.44 +shift $(($OPTIND - 1))
    2.45 +
    2.46 +
    2.47 +# args
    2.48 +
    2.49 +[ $# -ne 0 ] && usage
    2.50 +
    2.51 +
    2.52  ## main
    2.53  
    2.54  ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    2.55 @@ -27,7 +65,14 @@
    2.56  [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    2.57  [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    2.58  
    2.59 -$ISABELLE \
    2.60 -  -e "val ml_system = \"$ML_SYSTEM\";" \
    2.61 -  -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
    2.62 -  -q -w RAW_ML_SYSTEM Pure
    2.63 +if [ -z "$RAW" ]; then
    2.64 +  $ISABELLE \
    2.65 +    -e "val ml_system = \"$ML_SYSTEM\";" \
    2.66 +    -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
    2.67 +    -q -w RAW_ML_SYSTEM Pure
    2.68 +else
    2.69 +  $ISABELLE \
    2.70 +    -e "val ml_system = \"$ML_SYSTEM\";" \
    2.71 +    -e "use\"$COMPAT\";" \
    2.72 +    -q -w RAW_ML_SYSTEM RAW
    2.73 +fi