lib/scripts/run-polyml

tuned startup;
semi fix of piping-quit peoblem (should work on systems with *real& sh);

#!/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
}


## Poly/ML programs

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_HOME/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
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
  cp "$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
  sh -c "$ISABELLE_HOME/lib/Tools/symbolinput | $START_POLY"
  RC=$?
else
  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; } | $START_POLY"
  RC=$?
fi

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

exit $RC