some cygwin support;
authorwenzelm
Sat Jun 11 23:17:28 2005 +0200 (2005-06-11)
changeset 16374f4b7cf8975af
parent 16373 9d020423093b
child 16375 de1ab9e8ed4f
some cygwin support;
lib/scripts/run-polyml
src/Pure/ML-Systems/polyml.ML
     1.1 --- a/lib/scripts/run-polyml	Sat Jun 11 22:15:58 2005 +0200
     1.2 +++ b/lib/scripts/run-polyml	Sat Jun 11 23:17:28 2005 +0200
     1.3 @@ -29,7 +29,20 @@
     1.4  ## Poly/ML programs
     1.5  
     1.6  ML_DBASE_PREFIX=""
     1.7 -POLY="$ML_HOME/poly"
     1.8 +ML_DBASE_SUFFIX=""
     1.9 +CYGPATH=""
    1.10 +
    1.11 +case "$ML_PLATFORM" in
    1.12 +  *-cygwin)
    1.13 +    ML_DBASE_SUFFIX=".pmd"
    1.14 +    POLY="$ML_HOME/PolyML.exe"
    1.15 +    CYGPATH="cygpath -m"
    1.16 +    ;;
    1.17 +  *)
    1.18 +    POLY="$ML_HOME/poly"
    1.19 +    ;;
    1.20 +esac
    1.21 +
    1.22  check_file "$POLY"
    1.23  
    1.24  case "$ML_SYSTEM" in
    1.25 @@ -37,13 +50,13 @@
    1.26      if [ -z "$ML_DBASE" ]; then
    1.27        if [ -z "$COPYDB" ]; then
    1.28          ML_DBASE_PREFIX="$ML_HOME/"
    1.29 -        ML_DBASE="ML_dbase"
    1.30 +        ML_DBASE="ML_dbase${ML_DBASE_SUFFIX}"
    1.31        else
    1.32 -        ML_DBASE="$ML_HOME/ML_dbase"
    1.33 +        ML_DBASE="$ML_HOME/ML_dbase${ML_DBASE_SUFFIX}"
    1.34        fi
    1.35        POLYPATH="$ML_HOME"
    1.36      else
    1.37 -      POLYPATH=$(dirname "$ML_DBASE")
    1.38 +      POLYPATH="$(dirname "$ML_DBASE")"
    1.39      fi
    1.40      export POLYPATH
    1.41  
    1.42 @@ -96,7 +109,13 @@
    1.43    DB="$OUTFILE"
    1.44  else
    1.45    [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
    1.46 -  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
    1.47 +  if [ -z "$CYGPATH" ]; then
    1.48 +    echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
    1.49 +  else
    1.50 +    OUTFILE_CYGWIN="$($CYGPATH "$OUTFILE")"
    1.51 +    INFILE_CYGWIN="$($CYGPATH "$INFILE")"
    1.52 +    echo "PolyML.make_database \"$OUTFILE_CYGWIN\"; PolyML.quit();" | "$POLY" -r "$INFILE_CYGWIN"
    1.53 +  fi
    1.54    [ -f "$OUTFILE" ] || fail_out
    1.55    DB="$OUTFILE"
    1.56  fi
    1.57 @@ -112,8 +131,14 @@
    1.58  
    1.59  DB_INFO=$(ls -l "$DB" 2>/dev/null)
    1.60  
    1.61 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
    1.62 -  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.63 +if [ -z "$CYGPATH" ]; then
    1.64 +  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
    1.65 +    { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.66 +else
    1.67 +  DB_CYGWIN="$($CYGPATH "$DB")"
    1.68 +  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
    1.69 +    { read FPID; "$POLY" $ML_OPTIONS "$DB_CYGWIN"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.70 +fi
    1.71  RC="$?"
    1.72  
    1.73  NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Sat Jun 11 22:15:58 2005 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sat Jun 11 23:17:28 2005 +0200
     2.3 @@ -6,7 +6,17 @@
     2.4  Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x).
     2.5  *)
     2.6  
     2.7 -(** ML system related **)
     2.8 +(** ML system and platform related **)
     2.9 +
    2.10 +(* cygwin *)
    2.11 +
    2.12 +val cygwin_platform =
    2.13 +  let val n = size ml_platform
    2.14 +  in n >= 6 andalso String.substring (ml_platform, n - 6, 6) = "cygwin" end;
    2.15 +
    2.16 +fun if_cygwin f x = if cygwin_platform then f x else ();
    2.17 +fun unless_cygwin f x = if not cygwin_platform then f x else ();
    2.18 +
    2.19  
    2.20  (* old Poly/ML emulation *)
    2.21  
    2.22 @@ -34,7 +44,8 @@
    2.23  
    2.24  (* bounded time execution *)
    2.25  
    2.26 -use "ML-Systems/polyml-time-limit.ML";
    2.27 +unless_cygwin
    2.28 +  use "ML-Systems/polyml-time-limit.ML";
    2.29  
    2.30  
    2.31  (* prompts *)
    2.32 @@ -168,25 +179,5 @@
    2.33  val profiling: int->unit =
    2.34       RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;
    2.35  
    2.36 -structure OriginalPosix = Posix;
    2.37 -structure OriginalIO = Posix.IO;
    2.38 -
    2.39 -structure Posix =
    2.40 -struct
    2.41 -  open OriginalPosix
    2.42 -  structure IO =
    2.43 -  struct
    2.44 -  open OriginalIO
    2.45 -  val mkTextReader = mkReader
    2.46 -  val mkTextWriter = mkWriter
    2.47 -  end;
    2.48 -end;
    2.49 -
    2.50 -(*This extension of the Poly/ML Signal structure is only necessary
    2.51 -  because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
    2.52 -structure IsaSignal =
    2.53 -struct
    2.54 -  open Signal
    2.55 -  val usr1 = Posix.Signal.usr1
    2.56 -  val usr2 = Posix.Signal.usr2
    2.57 -end;
    2.58 +unless_cygwin
    2.59 +  use "ML-Systems/polyml-posix.ML";