src/Pure/mk

moved basic thm operations from structure PureThy to Thm;
added position operations;
tuned;

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# mk - build Pure Isabelle.
#
# Requires proper Isabelle settings environment (cf. IsaMakefile).


## diagnostics

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS]"
  echo
  echo "  Make Pure Isabelle."
  echo
  echo "    -R DIR/FILE  run RAW session"
  echo "    -r           build RAW image"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

RAW_SESSION=""
RAW=""

while getopts "R:r" OPT
do
  case "$OPT" in
    R)
      RAW_SESSION="$OPTARG"
      ;;
    r)
      RAW=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && usage


## main

# get compatibility file

ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"

COMPAT=""
[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"


# prepare log dir

LOGDIR="$ISABELLE_OUTPUT/log"
mkdir -p "$LOGDIR"


# run isabelle

. "$ISABELLE_HOME/lib/scripts/timestart.bash"

if [ -n "$RAW" ]; then
  ITEM="RAW"
  echo "Building $ITEM ..."
  LOG="$LOGDIR/$ITEM"

  "$ISABELLE" \
    -e "val ml_system = \"$ML_SYSTEM\";" \
    -e "val ml_platform = \"$ML_PLATFORM\";" \
    -e "use\"$COMPAT\" handle _ => exit 1;" \
    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
  RC="$?"
elif [ -n "$RAW_SESSION" ]; then
  ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
  echo "Running $ITEM ..."
  LOG="$LOGDIR/$ITEM"

  "$ISABELLE" \
    -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
    -q RAW > "$LOG" 2>&1
  RC="$?"
else
  ITEM="Pure"
  echo "Building $ITEM ..."
  LOG="$LOGDIR/$ITEM"

  "$ISABELLE" \
    -e "val ml_system = \"$ML_SYSTEM\";" \
    -e "val ml_platform = \"$ML_PLATFORM\";" \
    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
    -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
  RC="$?"
fi

. "$ISABELLE_HOME/lib/scripts/timestop.bash"


# exit status

if [ "$RC" -eq 0 ]; then
  echo "Finished $ITEM ($TIMES_REPORT)"
  gzip --force "$LOG"
else
  echo "$ITEM FAILED"
  echo "(see also $LOG)"
  echo; tail "$LOG"; echo
fi

exit "$RC"