lib/scripts/run-polyml

--- a/lib/scripts/run-polyml	Tue Jun 14 21:56:57 2005 +0200
+++ b/lib/scripts/run-polyml	Tue Jun 14 22:08:53 2005 +0200
@@ -26,57 +26,41 @@
 }
 
 
-## Poly/ML programs
+## Poly/ML executable and database
 
 ML_DBASE_PREFIX=""
 ML_DBASE_SUFFIX=""
-CYGPATH=""
 
 case "$ML_PLATFORM" in
   *-cygwin)
     ML_DBASE_SUFFIX=".pmd"
     POLY="$ML_HOME/PolyML.exe"
-    CYGPATH="cygpath -m"
+    function fixpath () { cygpath -m "$@"; }
     ;;
   *)
     POLY="$ML_HOME/poly"
+    function fixpath () { echo -n "$@"; }
     ;;
 esac
 
 check_file "$POLY"
 
-case "$ML_SYSTEM" in
-  polyml-4.*)
-    if [ -z "$ML_DBASE" ]; then
-      if [ -z "$COPYDB" ]; then
-        ML_DBASE_PREFIX="$ML_HOME/"
-        ML_DBASE="ML_dbase${ML_DBASE_SUFFIX}"
-      else
-        ML_DBASE="$ML_HOME/ML_dbase${ML_DBASE_SUFFIX}"
-      fi
-      POLYPATH="$ML_HOME"
-    else
-      POLYPATH="$(dirname "$ML_DBASE")"
-    fi
-    export POLYPATH
+if [ -z "$ML_DBASE" ]; then
+  if [ -z "$COPYDB" ]; then
+    ML_DBASE_PREFIX="$ML_HOME/"
+    ML_DBASE="ML_dbase${ML_DBASE_SUFFIX}"
+  else
+    ML_DBASE="$ML_HOME/ML_dbase${ML_DBASE_SUFFIX}"
+  fi
+  export POLYPATH="$(fixpath "$ML_HOME")"
+else
+  export POLYPATH="$(fixpath "$(dirname "$ML_DBASE")")"
+fi
 
-    DISCGARB="$POLY"
-    DISCGARB_OPTIONS="-d -c"
+DISCGARB="$POLY"
+DISCGARB_OPTIONS="-d -c"
 
-    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
-    ;;
-  *)
-    if [ -z "$ML_DBASE" ]; then
-      ML_DBASE="$ML_HOME/ML_dbase"
-    fi
-
-    DISCGARB="$ML_HOME/discgarb"
-    DISCGARB_OPTIONS="-c"
-    check_file "$DISCGARB"
-
-    EXIT="val exit = PolyML.exit;"
-    ;;
-esac
+EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
 
 
 ## prepare databases
@@ -109,13 +93,7 @@
   DB="$OUTFILE"
 else
   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
-  if [ -z "$CYGPATH" ]; then
-    echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
-  else
-    OUTFILE_CYGWIN="$($CYGPATH "$OUTFILE")"
-    INFILE_CYGWIN="$($CYGPATH "$INFILE")"
-    echo "PolyML.make_database \"$OUTFILE_CYGWIN\"; PolyML.quit();" | "$POLY" -r "$INFILE_CYGWIN"
-  fi
+  echo "PolyML.make_database \"$(fixpath "$OUTFILE")\"; PolyML.quit();" | "$POLY" -r "$(fixpath "$INFILE")"
   [ -f "$OUTFILE" ] || fail_out
   DB="$OUTFILE"
 fi
@@ -129,19 +107,14 @@
   FEEDER_OPTS="-q"
 fi
 
-DB_INFO=$(ls -l "$DB" 2>/dev/null)
+DB_INFO="$(ls -l "$DB" 2>/dev/null)"
 
-if [ -z "$CYGPATH" ]; then
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
-    { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-else
-  DB_CYGWIN="$($CYGPATH "$DB")"
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
-    { read FPID; "$POLY" $ML_OPTIONS "$DB_CYGWIN"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-fi
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
+  read FPID; "$POLY" $ML_OPTIONS "$(fixpath "$DB")";
+  RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"
 
-NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
+NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
   "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"