lib/scripts/run-polyml

replaced cat by ucat;
fixed RC handling;

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


## diagnostics

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



## locations and settings

ML_QUIT=";PolyML.quit();"
ML_DBASE=$ML_HOME/ML_dbase
POLY=$ML_HOME/poly
DISCGARB=$ML_HOME/discgarb

case "$ML_SYSTEM" in
  polyml-3.1)
    DISCGARB="$DISCGARB -c"
    export LM_LICENSE_FILE=$ML_HOME/license.dat
    ;;
esac



## prepare databases

if [ -z "$INFILE" ]; then
  INFILE="$ML_DBASE"
  MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT"
fi

function fail_out()
{
  fail "Unable to create output heap file: \"$OUTFILE\""
}

if [ -z "$OUTFILE" ]; then
  DB="$INFILE"
  OPTS="-r"  
elif [ "$INFILE" = "$OUTFILE" ]; then           # FIXME -ef !?
  DB="$INFILE"
  OPTS=""
elif [ -n "$COPYDB" ]; then
  cp "$INFILE" "$OUTFILE" || fail_out
  chmod +w "$OUTFILE"
  DB="$OUTFILE"
  OPTS=""
else
  [ -f "$OUTFILE" ] && { rm "$OUTFILE" || fail_out }
  echo "PolyML.make_database \"$OUTFILE\"; $ML_QUIT" | $POLY -r "$INFILE"
  [ -f "$OUTFILE" ] || fail_out
  DB="$OUTFILE"
  OPTS=""
fi



## run it!

START_POLY="$POLY $OPTS $ML_OPTIONS $OPTIONS $DB"

if [ -n "$TERMINATE" ]; then
  echo "$MLTEXT" "$ML_QUIT" | $START_POLY
  RC=$?
elif [ -z "$MLTEXT" ]; then
  $START_POLY
  RC=$?
else
  TMP_FILE=/tmp/mltext-$$
  echo "$MLTEXT" >$TMP_FILE
  $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_POLY
  RC=$?
  rm $TMP_FILE
fi

[ $RC -eq 0 -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE"

exit $RC