src/Pure/mk
author paulson
Fri May 30 15:14:59 1997 +0200 (1997-05-30)
changeset 3365 86c0d1988622
parent 3118 24dae6222579
child 3505 1cb4ea47d967
permissions -rwxr-xr-x
flushOut ensures that no recent error message are lost (not certain this is
necessary)
     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 fail()
    13 {
    14   echo "$1" >&2
    15   exit 2
    16 }
    17 
    18 
    19 ## main
    20 
    21 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    22 [ -z "$ML_SYSTEM" ] && \
    23   fail "Missing ML system settings! Probably not run via 'isatool make'?."
    24 
    25 COMPAT=""
    26 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
    27 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
    28 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
    29 
    30 $ISABELLE \
    31   -e "val ml_system = \"$ML_SYSTEM\";" \
    32   -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
    33   -q RAW_ML_SYSTEM Pure
    34 
    35 chmod -w $ISABELLE_OUTPUT/Pure