lib/scripts/run-polyml

now discgarb called only for changed databases;

#!/bin/bash -norc
#
# $Id$
#
# Poly/ML startup script.
#
# Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE,
# and from settings


## diagnostics

function fail_out()
{
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
  exit 2
}


## locations and settings

ML_DBASE=$ML_HOME/ML_dbase
POLY=$ML_HOME/poly
DISCGARB=$ML_HOME/discgarb

case "$ML_SYSTEM" in
  polyml-3.*)
    DISCGARB="$DISCGARB -c"
    ;;
esac


## prepare databases

MLINIT=""

if [ -z "$INFILE" ]; then
  INFILE="$ML_DBASE"
  MLINIT="val use = PolyML.use; val exit = PolyML.exit; fun init_database () = ();"
fi

if [ -z "$OUTFILE" ]; then
  DB="$INFILE"
  ML_OPTIONS="-r $ML_OPTIONS"  
elif [ "$INFILE" -ef "$OUTFILE" ]; then
  DB="$INFILE"
elif [ -n "$COPYDB" ]; then
  cp -f "$INFILE" "$OUTFILE" || fail_out
  chmod +w "$OUTFILE" || fail_out
  DB="$OUTFILE"
else
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
  [ -f "$OUTFILE" ] || fail_out
  DB="$OUTFILE"
  MLINIT="$MLINIT init_database ();"
fi


## run it!

START_POLY="$POLY $ML_OPTIONS $DB"
DB_INFO=$(ls -l $DB)

[ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT"

if [ -n "$TERMINATE" ]; then
  echo "$MLTEXT" | $START_POLY
  RC=$?
elif [ -z "$MLTEXT" ]; then
  $START_POLY
  RC=$?
else
  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat } | $START_POLY
  RC=$?
fi

NEW_DB_INFO=$(ls -l $DB)
[ $RC -eq 0 -a -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"

exit $RC