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