lib/scripts/run-polyml
changeset 10206 d48a2e324abf
parent 10105 f9be78009930
child 10555 2323ec838401
     1.1 --- a/lib/scripts/run-polyml	Thu Oct 12 17:47:32 2000 +0200
     1.2 +++ b/lib/scripts/run-polyml	Thu Oct 12 17:48:06 2000 +0200
     1.3 @@ -17,11 +17,11 @@
     1.4    exit 2
     1.5  }
     1.6  
     1.7 -function check_mlhome_file()
     1.8 +function check_file()
     1.9  {
    1.10    if [ ! -f "$1" ]; then
    1.11      echo "Unable to locate $1" >&2
    1.12 -    echo "Please check your ML_HOME setting!" >&2
    1.13 +    echo "Please check your ML system settings!" >&2
    1.14      exit 2
    1.15    fi
    1.16  }
    1.17 @@ -29,18 +29,39 @@
    1.18  
    1.19  ## Poly/ML programs
    1.20  
    1.21 +ML_DBASE_PREFIX=""
    1.22  POLY="$ML_HOME/poly"
    1.23 -DISCGARB="$ML_HOME/discgarb"
    1.24 -
    1.25 -check_mlhome_file "$POLY"
    1.26 -check_mlhome_file "$DISCGARB"
    1.27 -
    1.28 +check_file "$POLY"
    1.29  
    1.30  case "$ML_SYSTEM" in
    1.31    polyml-4.*)
    1.32 +    if [ -z "$ML_DBASE" ]; then
    1.33 +      if [ -z "$COPYDB" ]; then
    1.34 +        ML_DBASE_PREFIX="$ML_HOME/"
    1.35 +        ML_DBASE="ML_dbase"
    1.36 +      else
    1.37 +        ML_DBASE="$ML_HOME/ML_dbase"
    1.38 +      fi
    1.39 +      POLYPATH="$ML_HOME"
    1.40 +    else
    1.41 +      POLYPATH=$(dirname "$ML_DBASE")
    1.42 +    fi
    1.43 +    export POLYPATH
    1.44 +
    1.45 +    DISCGARB="$POLY"
    1.46 +    DISCGARB_OPTIONS="-d -c"
    1.47 +
    1.48      EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    1.49      ;;
    1.50    *)
    1.51 +    if [ -z "$ML_DBASE" ]; then
    1.52 +      ML_DBASE="$ML_HOME/ML_dbase"
    1.53 +    fi
    1.54 +
    1.55 +    DISCGARB="$ML_HOME/discgarb"
    1.56 +    DISCGARB_OPTIONS="-c"
    1.57 +    check_file "$DISCGARB"
    1.58 +
    1.59      EXIT="val exit = PolyML.exit;"
    1.60      ;;
    1.61  esac
    1.62 @@ -49,8 +70,8 @@
    1.63  ## prepare databases
    1.64  
    1.65  if [ -z "$INFILE" ]; then
    1.66 -  INFILE="$ML_HOME/ML_dbase"
    1.67 -  check_mlhome_file "$INFILE"
    1.68 +  check_file "$ML_DBASE_PREFIX$ML_DBASE"
    1.69 +  INFILE="$ML_DBASE"
    1.70    MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
    1.71  else
    1.72    COPYDB=true
    1.73 @@ -82,14 +103,15 @@
    1.74    FEEDER_OPTS="-q"
    1.75  fi
    1.76  
    1.77 -DB_INFO=$(ls -l "$DB")
    1.78 +DB_INFO=$(ls -l "$DB" 2>/dev/null)
    1.79  
    1.80  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
    1.81    { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.82  RC="$?"
    1.83  
    1.84 -NEW_DB_INFO=$(ls -l "$DB")
    1.85 -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && "$DISCGARB" -c "$OUTFILE"
    1.86 +NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
    1.87 +[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
    1.88 +  "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"
    1.89  [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    1.90  
    1.91  exit "$RC"