lib/scripts/run-polyml
author wenzelm
Mon Dec 02 18:24:01 1996 +0100 (1996-12-02)
changeset 2301 c72f4f7236b6
child 2314 67bf78c7c725
permissions -rwxr-xr-x
run-polyml: Poly/ML startup script.
wenzelm@2301
     1
#!/bin/bash
wenzelm@2301
     2
#
wenzelm@2301
     3
# Poly/ML startup script.
wenzelm@2301
     4
#
wenzelm@2301
     5
# $Id$
wenzelm@2301
     6
#
wenzelm@2301
     7
# Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE,
wenzelm@2301
     8
# and from settings
wenzelm@2301
     9
#
wenzelm@2301
    10
# MMW 22-Nov-1996, MMW 25-Nov-1996
wenzelm@2301
    11
wenzelm@2301
    12
wenzelm@2301
    13
## diagnostics
wenzelm@2301
    14
wenzelm@2301
    15
function fail()
wenzelm@2301
    16
{
wenzelm@2301
    17
  echo "$1"
wenzelm@2301
    18
  exit 2
wenzelm@2301
    19
}
wenzelm@2301
    20
wenzelm@2301
    21
wenzelm@2301
    22
wenzelm@2301
    23
## locations and settings
wenzelm@2301
    24
wenzelm@2301
    25
ML_QUIT=";PolyML.quit();"
wenzelm@2301
    26
ML_DBASE=$ML_HOME/ML_dbase
wenzelm@2301
    27
POLY=$ML_HOME/poly
wenzelm@2301
    28
DISCGARB=$ML_HOME/discgarb
wenzelm@2301
    29
wenzelm@2301
    30
case "$ML_SYSTEM" in
wenzelm@2301
    31
  polyml-2.07)
wenzelm@2301
    32
    ;;
wenzelm@2301
    33
  polyml-3.1)
wenzelm@2301
    34
    DISCGARB="$ML_HOME/discgarb -c"
wenzelm@2301
    35
    export LM_LICENSE_FILE=$ML_HOME/license.dat
wenzelm@2301
    36
    ;;
wenzelm@2301
    37
  *)
wenzelm@2301
    38
    fail "Unknown ML system: \"$ML_SYSTEM\""
wenzelm@2301
    39
    ;;
wenzelm@2301
    40
esac
wenzelm@2301
    41
wenzelm@2301
    42
wenzelm@2301
    43
wenzelm@2301
    44
## prepare databases
wenzelm@2301
    45
wenzelm@2301
    46
if [ -z "$INFILE" ]; then
wenzelm@2301
    47
  INFILE="$ML_DBASE"
wenzelm@2301
    48
  MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT"
wenzelm@2301
    49
fi
wenzelm@2301
    50
wenzelm@2301
    51
function fail_out()
wenzelm@2301
    52
{
wenzelm@2301
    53
  fail "Unable to create output heap file: \"$OUTFILE\""
wenzelm@2301
    54
}
wenzelm@2301
    55
wenzelm@2301
    56
if [ -z "$OUTFILE" ]; then
wenzelm@2301
    57
  DB="$INFILE"
wenzelm@2301
    58
  OPTS="-r"  
wenzelm@2301
    59
elif [ "$INFILE" = "$OUTFILE" ]; then           # FIXME -ef !?
wenzelm@2301
    60
  DB="$INFILE"
wenzelm@2301
    61
  OPTS=""
wenzelm@2301
    62
elif [ -n "$COPYDB" ]; then
wenzelm@2301
    63
  cp "$INFILE" "$OUTFILE" || fail_out
wenzelm@2301
    64
  chmod +w "$OUTFILE"
wenzelm@2301
    65
  DB="$OUTFILE"
wenzelm@2301
    66
  OPTS=""
wenzelm@2301
    67
else
wenzelm@2301
    68
  [ -f "$OUTFILE" ] && { rm "$OUTFILE" || fail_out }
wenzelm@2301
    69
  echo "PolyML.make_database \"$OUTFILE\"; $ML_QUIT" | $POLY -r "$INFILE"
wenzelm@2301
    70
  [ -f "$OUTFILE" ] || fail_out
wenzelm@2301
    71
  DB="$OUTFILE"
wenzelm@2301
    72
  OPTS=""
wenzelm@2301
    73
fi
wenzelm@2301
    74
wenzelm@2301
    75
wenzelm@2301
    76
wenzelm@2301
    77
## run it!
wenzelm@2301
    78
wenzelm@2301
    79
START_POLY="$POLY $OPTS $ML_OPTIONS $OPTIONS $DB"
wenzelm@2301
    80
wenzelm@2301
    81
if [ -n "$TERMINATE" ]; then
wenzelm@2301
    82
  echo "$MLTEXT" "$ML_QUIT" | $START_POLY
wenzelm@2301
    83
  RC=$?
wenzelm@2301
    84
elif [ -z "$MLTEXT" ]; then
wenzelm@2301
    85
  $START_POLY
wenzelm@2301
    86
  RC=$?
wenzelm@2301
    87
else
wenzelm@2301
    88
  TMP_FILE=/tmp/mltext-$$
wenzelm@2301
    89
  echo "$MLTEXT" >$TMP_FILE
wenzelm@2301
    90
  cat $TMP_FILE - | $START_POLY
wenzelm@2301
    91
  RC=$?
wenzelm@2301
    92
  rm $TMP_FILE
wenzelm@2301
    93
fi
wenzelm@2301
    94
wenzelm@2301
    95
[ $RC -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE"
wenzelm@2301
    96
wenzelm@2301
    97
exit $RC