src/Pure/mk
author nipkow
Fri Nov 28 07:35:10 1997 +0100 (1997-11-28)
changeset 4318 9b672ea2dfe7
parent 3774 b1bfd394b60a
child 4442 8ed9e689a15e
permissions -rwxr-xr-x
Fixed the definition of `termord': is now antisymmetric.
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # mk - build Pure Isabelle.
     6 #
     7 # Assumes to be called via Isabelle make utility (cf. IsaMakefile).
     8 
     9 
    10 ## diagnostics
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [OPTIONS]"
    16   echo
    17   echo "  Make Pure Isabelle."
    18   echo
    19   echo "    -r           just prepare RAW image"
    20   echo
    21   exit 1
    22 }
    23 
    24 function fail()
    25 {
    26   echo "$1" >&2
    27   exit 2
    28 }
    29 
    30 
    31 ## process command line
    32 
    33 # options
    34 
    35 RAW=""
    36 
    37 while getopts "r" OPT
    38 do
    39   case "$OPT" in
    40     r)
    41       RAW=true
    42       ;;
    43     \?)
    44       usage
    45       ;;
    46   esac
    47 done
    48 
    49 shift $(($OPTIND - 1))
    50 
    51 
    52 # args
    53 
    54 [ $# -ne 0 ] && usage
    55 
    56 
    57 ## main
    58 
    59 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    60 [ -z "$ML_SYSTEM" ] && \
    61   fail "Missing ML system settings! Probably not run via 'isatool make'?."
    62 
    63 COMPAT=""
    64 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
    65 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    66 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    67 
    68 if [ -z "$RAW" ]; then
    69   $ISABELLE \
    70     -e "val ml_system = \"$ML_SYSTEM\";" \
    71     -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
    72     -q -w RAW_ML_SYSTEM Pure
    73 else
    74   $ISABELLE \
    75     -e "val ml_system = \"$ML_SYSTEM\";" \
    76     -e "use\"$COMPAT\";" \
    77     -q -w RAW_ML_SYSTEM RAW
    78 fi