some cygwin support;

--- 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)

--- a/src/Pure/ML-Systems/polyml.ML	Sat Jun 11 22:15:58 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Jun 11 23:17:28 2005 +0200
@@ -6,7 +6,17 @@
 Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x).
 *)
 
-(** ML system related **)
+(** ML system and platform related **)
+
+(* cygwin *)
+
+val cygwin_platform =
+  let val n = size ml_platform
+  in n >= 6 andalso String.substring (ml_platform, n - 6, 6) = "cygwin" end;
+
+fun if_cygwin f x = if cygwin_platform then f x else ();
+fun unless_cygwin f x = if not cygwin_platform then f x else ();
+
 
 (* old Poly/ML emulation *)
 
@@ -34,7 +44,8 @@
 
 (* bounded time execution *)
 
-use "ML-Systems/polyml-time-limit.ML";
+unless_cygwin
+  use "ML-Systems/polyml-time-limit.ML";
 
 
 (* prompts *)
@@ -168,25 +179,5 @@
 val profiling: int->unit =
      RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;
 
-structure OriginalPosix = Posix;
-structure OriginalIO = Posix.IO;
-
-structure Posix =
-struct
-  open OriginalPosix
-  structure IO =
-  struct
-  open OriginalIO
-  val mkTextReader = mkReader
-  val mkTextWriter = mkWriter
-  end;
-end;
-
-(*This extension of the Poly/ML Signal structure is only necessary
-  because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
-structure IsaSignal =
-struct
-  open Signal
-  val usr1 = Posix.Signal.usr1
-  val usr2 = Posix.Signal.usr2
-end;
+unless_cygwin
+  use "ML-Systems/polyml-posix.ML";