lib/scripts/run-polyml

--- a/lib/scripts/run-polyml	Sat Jun 11 22:15:58 2005 +0200
+++ b/lib/scripts/run-polyml	Sat Jun 11 23:17:28 2005 +0200
@@ -29,7 +29,20 @@
 ## Poly/ML programs
 
 ML_DBASE_PREFIX=""
-POLY="$ML_HOME/poly"
+ML_DBASE_SUFFIX=""
+CYGPATH=""
+
+case "$ML_PLATFORM" in
+  *-cygwin)
+    ML_DBASE_SUFFIX=".pmd"
+    POLY="$ML_HOME/PolyML.exe"
+    CYGPATH="cygpath -m"
+    ;;
+  *)
+    POLY="$ML_HOME/poly"
+    ;;
+esac
+
 check_file "$POLY"
 
 case "$ML_SYSTEM" in
@@ -37,13 +50,13 @@
     if [ -z "$ML_DBASE" ]; then
       if [ -z "$COPYDB" ]; then
         ML_DBASE_PREFIX="$ML_HOME/"
-        ML_DBASE="ML_dbase"
+        ML_DBASE="ML_dbase${ML_DBASE_SUFFIX}"
       else
-        ML_DBASE="$ML_HOME/ML_dbase"
+        ML_DBASE="$ML_HOME/ML_dbase${ML_DBASE_SUFFIX}"
       fi
       POLYPATH="$ML_HOME"
     else
-      POLYPATH=$(dirname "$ML_DBASE")
+      POLYPATH="$(dirname "$ML_DBASE")"
     fi
     export POLYPATH
 
@@ -96,7 +109,13 @@
   DB="$OUTFILE"
 else
   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
-  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
+  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
   [ -f "$OUTFILE" ] || fail_out
   DB="$OUTFILE"
 fi
@@ -112,8 +131,14 @@
 
 DB_INFO=$(ls -l "$DB" 2>/dev/null)
 
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
-  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+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
 RC="$?"
 
 NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)