1.1 --- a/Admin/CHECKLIST Sat May 30 22:37:38 2009 +0200
1.2 +++ b/Admin/CHECKLIST Sun May 31 14:15:07 2009 +0200
1.3 @@ -1,8 +1,9 @@
1.4 Checklist for official releases
1.5 ===============================
1.6
1.7 -- test mosml, polyml-5.2, polyml-5.1, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0,
1.8 - sparc-solaris, x86-solaris;
1.9 +- test mosml, polyml-5.2, polyml-5.1, polyml-5.0;
1.10 +
1.11 +- test sparc-solaris, x86-solaris;
1.12
1.13 - test ProofGeneral;
1.14
2.1 --- a/Admin/isatest/settings/at-poly-4.1.3 Sat May 30 22:37:38 2009 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,27 +0,0 @@
2.4 -# -*- shell-script -*-
2.5 -
2.6 - POLYML_HOME="/home/polyml/polyml-4.1.3"
2.7 - ML_SYSTEM="polyml-4.1.3"
2.8 - ML_PLATFORM="x86-linux"
2.9 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
2.10 - ML_OPTIONS="-h 30000"
2.11 -
2.12 -ISABELLE_HOME_USER=~/isabelle-at-poly-4.1.3
2.13 -
2.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
2.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
2.16 -
2.17 -# Location for temporary files (should be on a local file system).
2.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
2.19 -
2.20 -
2.21 -# Heap input locations. ML system identifier is included in lookup.
2.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
2.23 -
2.24 -# Heap output location. ML system identifier is appended automatically later on.
2.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
2.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
2.27 -
2.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
2.29 -
2.30 -HOL_USEDIR_OPTIONS="-p 2"
3.1 --- a/Admin/isatest/settings/at-poly-e Sat May 30 22:37:38 2009 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,27 +0,0 @@
3.4 -# -*- shell-script -*-
3.5 -
3.6 - POLYML_HOME="/home/polyml/polyml-4.2.0"
3.7 - ML_SYSTEM="polyml-4.2.0"
3.8 - ML_PLATFORM="x86-linux"
3.9 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
3.10 - ML_OPTIONS="-h 30000"
3.11 -
3.12 -ISABELLE_HOME_USER=~/isabelle-at-poly-e
3.13 -
3.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
3.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
3.16 -
3.17 -# Location for temporary files (should be on a local file system).
3.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
3.19 -
3.20 -
3.21 -# Heap input locations. ML system identifier is included in lookup.
3.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
3.23 -
3.24 -# Heap output location. ML system identifier is appended automatically later on.
3.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
3.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
3.27 -
3.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
3.29 -
3.30 -HOL_USEDIR_OPTIONS="-p 2"
4.1 --- a/NEWS Sat May 30 22:37:38 2009 +0200
4.2 +++ b/NEWS Sun May 31 14:15:07 2009 +0200
4.3 @@ -33,6 +33,11 @@
4.4 Attrib/Method.setup introduced in Isabelle2009.
4.5
4.6
4.7 +*** System ***
4.8 +
4.9 +* Discontinued support for Poly/ML 4.x versions.
4.10 +
4.11 +
4.12
4.13 New in Isabelle2009 (April 2009)
4.14 --------------------------------
5.1 --- a/etc/settings Sat May 30 22:37:38 2009 +0200
5.2 +++ b/etc/settings Sun May 31 14:15:07 2009 +0200
5.3 @@ -15,7 +15,7 @@
5.4 # not invent new ML system names unless you know what you are doing.
5.5 # Only one of the sections below should be activated.
5.6
5.7 -# Poly/ML 4.x/5.x (automated settings)
5.8 +# Poly/ML 5.x (automated settings)
5.9 POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
5.10 ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
5.11 ML_HOME=$(choosefrom \
5.12 @@ -41,12 +41,6 @@
5.13 #ML_SYSTEM=polyml-5.1
5.14 #ML_OPTIONS="-H 1000"
5.15
5.16 -# Poly/ML 4.2.0
5.17 -#ML_PLATFORM=x86-linux
5.18 -#ML_HOME=/usr/local/polyml/x86-linux
5.19 -#ML_SYSTEM=polyml-4.2.0
5.20 -#ML_OPTIONS="-H 80"
5.21 -
5.22 # Standard ML of New Jersey (slow!)
5.23 #ML_SYSTEM=smlnj-110
5.24 #ML_HOME="/usr/local/smlnj/bin"
6.1 --- a/lib/scripts/run-polyml-4.1.3 Sat May 30 22:37:38 2009 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,106 +0,0 @@
6.4 -#!/usr/bin/env bash
6.5 -#
6.6 -# Author: Markus Wenzel, TU Muenchen
6.7 -#
6.8 -# Poly/ML 4.x startup script.
6.9 -
6.10 -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
6.11 -
6.12 -
6.13 -## diagnostics
6.14 -
6.15 -function fail_out()
6.16 -{
6.17 - echo "Unable to create output heap file: \"$OUTFILE\"" >&2
6.18 - exit 2
6.19 -}
6.20 -
6.21 -function check_file()
6.22 -{
6.23 - if [ ! -f "$1" ]; then
6.24 - echo "Unable to locate $1" >&2
6.25 - echo "Please check your ML system settings!" >&2
6.26 - exit 2
6.27 - fi
6.28 -}
6.29 -
6.30 -
6.31 -## Poly/ML executable and database
6.32 -
6.33 -ML_DBASE_PREFIX=""
6.34 -
6.35 -POLY="$ML_HOME/poly"
6.36 -check_file "$POLY"
6.37 -
6.38 -if [ -z "$ML_DBASE" ]; then
6.39 - if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
6.40 - ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
6.41 - else
6.42 - ML_DBASE_HOME="$ML_HOME"
6.43 - fi
6.44 - if [ -z "$COPYDB" ]; then
6.45 - ML_DBASE_PREFIX="$ML_DBASE_HOME/"
6.46 - ML_DBASE="ML_dbase"
6.47 - else
6.48 - ML_DBASE="$ML_DBASE_HOME/ML_dbase"
6.49 - fi
6.50 - export POLYPATH="$ML_DBASE_HOME"
6.51 -else
6.52 - export POLYPATH="$(dirname "$ML_DBASE")"
6.53 -fi
6.54 -
6.55 -DISCGARB_OPTIONS="-d -c"
6.56 -
6.57 -EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
6.58 -
6.59 -
6.60 -## prepare databases
6.61 -
6.62 -if [ -z "$INFILE" ]; then
6.63 - check_file "$ML_DBASE_PREFIX$ML_DBASE"
6.64 - INFILE="$ML_DBASE"
6.65 - MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
6.66 - DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
6.67 -else
6.68 - COPYDB=true
6.69 -fi
6.70 -
6.71 -if [ -z "$OUTFILE" ]; then
6.72 - DB="$INFILE"
6.73 - ML_OPTIONS="-r $ML_OPTIONS"
6.74 -elif [ "$INFILE" -ef "$OUTFILE" ]; then
6.75 - DB="$INFILE"
6.76 -elif [ -n "$COPYDB" ]; then
6.77 - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
6.78 - cp "$INFILE" "$OUTFILE" || fail_out
6.79 - chmod +w "$OUTFILE" || fail_out
6.80 - DB="$OUTFILE"
6.81 -else
6.82 - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
6.83 - echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
6.84 - [ -f "$OUTFILE" ] || fail_out
6.85 - DB="$OUTFILE"
6.86 -fi
6.87 -
6.88 -
6.89 -## run it!
6.90 -
6.91 -if [ -z "$TERMINATE" ]; then
6.92 - FEEDER_OPTS=""
6.93 -else
6.94 - FEEDER_OPTS="-q"
6.95 -fi
6.96 -
6.97 -DB_INFO="$(ls -l "$DB" 2>/dev/null)"
6.98 -
6.99 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
6.100 - read FPID; "$POLY" $ML_OPTIONS "$DB";
6.101 - RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
6.102 -RC="$?"
6.103 -
6.104 -NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
6.105 -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
6.106 - "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
6.107 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
6.108 -
6.109 -exit "$RC"
7.1 --- a/lib/scripts/run-polyml-4.1.4 Sat May 30 22:37:38 2009 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,106 +0,0 @@
7.4 -#!/usr/bin/env bash
7.5 -#
7.6 -# Author: Markus Wenzel, TU Muenchen
7.7 -#
7.8 -# Poly/ML 4.x startup script.
7.9 -
7.10 -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
7.11 -
7.12 -
7.13 -## diagnostics
7.14 -
7.15 -function fail_out()
7.16 -{
7.17 - echo "Unable to create output heap file: \"$OUTFILE\"" >&2
7.18 - exit 2
7.19 -}
7.20 -
7.21 -function check_file()
7.22 -{
7.23 - if [ ! -f "$1" ]; then
7.24 - echo "Unable to locate $1" >&2
7.25 - echo "Please check your ML system settings!" >&2
7.26 - exit 2
7.27 - fi
7.28 -}
7.29 -
7.30 -
7.31 -## Poly/ML executable and database
7.32 -
7.33 -ML_DBASE_PREFIX=""
7.34 -
7.35 -POLY="$ML_HOME/poly"
7.36 -check_file "$POLY"
7.37 -
7.38 -if [ -z "$ML_DBASE" ]; then
7.39 - if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
7.40 - ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
7.41 - else
7.42 - ML_DBASE_HOME="$ML_HOME"
7.43 - fi
7.44 - if [ -z "$COPYDB" ]; then
7.45 - ML_DBASE_PREFIX="$ML_DBASE_HOME/"
7.46 - ML_DBASE="ML_dbase"
7.47 - else
7.48 - ML_DBASE="$ML_DBASE_HOME/ML_dbase"
7.49 - fi
7.50 - export POLYPATH="$ML_DBASE_HOME"
7.51 -else
7.52 - export POLYPATH="$(dirname "$ML_DBASE")"
7.53 -fi
7.54 -
7.55 -DISCGARB_OPTIONS="-d -c"
7.56 -
7.57 -EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
7.58 -
7.59 -
7.60 -## prepare databases
7.61 -
7.62 -if [ -z "$INFILE" ]; then
7.63 - check_file "$ML_DBASE_PREFIX$ML_DBASE"
7.64 - INFILE="$ML_DBASE"
7.65 - MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
7.66 - DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
7.67 -else
7.68 - COPYDB=true
7.69 -fi
7.70 -
7.71 -if [ -z "$OUTFILE" ]; then
7.72 - DB="$INFILE"
7.73 - ML_OPTIONS="-r $ML_OPTIONS"
7.74 -elif [ "$INFILE" -ef "$OUTFILE" ]; then
7.75 - DB="$INFILE"
7.76 -elif [ -n "$COPYDB" ]; then
7.77 - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
7.78 - cp "$INFILE" "$OUTFILE" || fail_out
7.79 - chmod +w "$OUTFILE" || fail_out
7.80 - DB="$OUTFILE"
7.81 -else
7.82 - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
7.83 - echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
7.84 - [ -f "$OUTFILE" ] || fail_out
7.85 - DB="$OUTFILE"
7.86 -fi
7.87 -
7.88 -
7.89 -## run it!
7.90 -
7.91 -if [ -z "$TERMINATE" ]; then
7.92 - FEEDER_OPTS=""
7.93 -else
7.94 - FEEDER_OPTS="-q"
7.95 -fi
7.96 -
7.97 -DB_INFO="$(ls -l "$DB" 2>/dev/null)"
7.98 -
7.99 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
7.100 - read FPID; "$POLY" $ML_OPTIONS "$DB";
7.101 - RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
7.102 -RC="$?"
7.103 -
7.104 -NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
7.105 -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
7.106 - "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
7.107 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
7.108 -
7.109 -exit "$RC"
8.1 --- a/lib/scripts/run-polyml-4.2.0 Sat May 30 22:37:38 2009 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,106 +0,0 @@
8.4 -#!/usr/bin/env bash
8.5 -#
8.6 -# Author: Markus Wenzel, TU Muenchen
8.7 -#
8.8 -# Poly/ML 4.x startup script.
8.9 -
8.10 -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
8.11 -
8.12 -
8.13 -## diagnostics
8.14 -
8.15 -function fail_out()
8.16 -{
8.17 - echo "Unable to create output heap file: \"$OUTFILE\"" >&2
8.18 - exit 2
8.19 -}
8.20 -
8.21 -function check_file()
8.22 -{
8.23 - if [ ! -f "$1" ]; then
8.24 - echo "Unable to locate $1" >&2
8.25 - echo "Please check your ML system settings!" >&2
8.26 - exit 2
8.27 - fi
8.28 -}
8.29 -
8.30 -
8.31 -## Poly/ML executable and database
8.32 -
8.33 -ML_DBASE_PREFIX=""
8.34 -
8.35 -POLY="$ML_HOME/poly"
8.36 -check_file "$POLY"
8.37 -
8.38 -if [ -z "$ML_DBASE" ]; then
8.39 - if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
8.40 - ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
8.41 - else
8.42 - ML_DBASE_HOME="$ML_HOME"
8.43 - fi
8.44 - if [ -z "$COPYDB" ]; then
8.45 - ML_DBASE_PREFIX="$ML_DBASE_HOME/"
8.46 - ML_DBASE="ML_dbase"
8.47 - else
8.48 - ML_DBASE="$ML_DBASE_HOME/ML_dbase"
8.49 - fi
8.50 - export POLYPATH="$ML_DBASE_HOME"
8.51 -else
8.52 - export POLYPATH="$(dirname "$ML_DBASE")"
8.53 -fi
8.54 -
8.55 -DISCGARB_OPTIONS="-d -c"
8.56 -
8.57 -EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
8.58 -
8.59 -
8.60 -## prepare databases
8.61 -
8.62 -if [ -z "$INFILE" ]; then
8.63 - check_file "$ML_DBASE_PREFIX$ML_DBASE"
8.64 - INFILE="$ML_DBASE"
8.65 - MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
8.66 - DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
8.67 -else
8.68 - COPYDB=true
8.69 -fi
8.70 -
8.71 -if [ -z "$OUTFILE" ]; then
8.72 - DB="$INFILE"
8.73 - ML_OPTIONS="-r $ML_OPTIONS"
8.74 -elif [ "$INFILE" -ef "$OUTFILE" ]; then
8.75 - DB="$INFILE"
8.76 -elif [ -n "$COPYDB" ]; then
8.77 - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
8.78 - cp "$INFILE" "$OUTFILE" || fail_out
8.79 - chmod +w "$OUTFILE" || fail_out
8.80 - DB="$OUTFILE"
8.81 -else
8.82 - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
8.83 - echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
8.84 - [ -f "$OUTFILE" ] || fail_out
8.85 - DB="$OUTFILE"
8.86 -fi
8.87 -
8.88 -
8.89 -## run it!
8.90 -
8.91 -if [ -z "$TERMINATE" ]; then
8.92 - FEEDER_OPTS=""
8.93 -else
8.94 - FEEDER_OPTS="-q"
8.95 -fi
8.96 -
8.97 -DB_INFO="$(ls -l "$DB" 2>/dev/null)"
8.98 -
8.99 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
8.100 - read FPID; "$POLY" $ML_OPTIONS "$DB";
8.101 - RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
8.102 -RC="$?"
8.103 -
8.104 -NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
8.105 -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
8.106 - "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
8.107 -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
8.108 -
8.109 -exit "$RC"
9.1 --- a/src/Pure/IsaMakefile Sat May 30 22:37:38 2009 +0200
9.2 +++ b/src/Pure/IsaMakefile Sun May 31 14:15:07 2009 +0200
9.3 @@ -22,11 +22,9 @@
9.4 BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
9.5 ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
9.6 ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
9.7 - ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \
9.8 - ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \
9.9 - ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
9.10 - ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML \
9.11 - ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML \
9.12 + ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
9.13 + ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
9.14 + ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
9.15 ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \
9.16 ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
9.17 ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
10.1 --- a/src/Pure/ML-Systems/polyml-4.1.3.ML Sat May 30 22:37:38 2009 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,15 +0,0 @@
10.4 -(* Title: Pure/ML-Systems/polyml-4.1.3.ML
10.5 -
10.6 -Compatibility wrapper for Poly/ML 4.1.3.
10.7 -*)
10.8 -
10.9 -use "ML-Systems/polyml_old_basis.ML";
10.10 -use "ML-Systems/universal.ML";
10.11 -use "ML-Systems/thread_dummy.ML";
10.12 -use "ML-Systems/ml_name_space.ML";
10.13 -use "ML-Systems/polyml_common.ML";
10.14 -use "ML-Systems/polyml_old_compiler4.ML";
10.15 -use "ML-Systems/polyml_pp.ML";
10.16 -
10.17 -val pointer_eq = Address.wordEq;
10.18 -
11.1 --- a/src/Pure/ML-Systems/polyml-4.1.4.ML Sat May 30 22:37:38 2009 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,15 +0,0 @@
11.4 -(* Title: Pure/ML-Systems/polyml-4.1.4.ML
11.5 -
11.6 -Compatibility wrapper for Poly/ML 4.1.4.
11.7 -*)
11.8 -
11.9 -use "ML-Systems/polyml_old_basis.ML";
11.10 -use "ML-Systems/universal.ML";
11.11 -use "ML-Systems/thread_dummy.ML";
11.12 -use "ML-Systems/ml_name_space.ML";
11.13 -use "ML-Systems/polyml_common.ML";
11.14 -use "ML-Systems/polyml_old_compiler4.ML";
11.15 -use "ML-Systems/polyml_pp.ML";
11.16 -
11.17 -val pointer_eq = Address.wordEq;
11.18 -
12.1 --- a/src/Pure/ML-Systems/polyml-4.2.0.ML Sat May 30 22:37:38 2009 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,14 +0,0 @@
12.4 -(* Title: Pure/ML-Systems/polyml-4.2.0.ML
12.5 -
12.6 -Compatibility wrapper for Poly/ML 4.2.0.
12.7 -*)
12.8 -
12.9 -use "ML-Systems/universal.ML";
12.10 -use "ML-Systems/thread_dummy.ML";
12.11 -use "ML-Systems/ml_name_space.ML";
12.12 -use "ML-Systems/polyml_common.ML";
12.13 -use "ML-Systems/polyml_old_compiler4.ML";
12.14 -use "ML-Systems/polyml_pp.ML";
12.15 -
12.16 -val pointer_eq = Address.wordEq;
12.17 -
13.1 --- a/src/Pure/ML-Systems/polyml_common.ML Sat May 30 22:37:38 2009 +0200
13.2 +++ b/src/Pure/ML-Systems/polyml_common.ML Sun May 31 14:15:07 2009 +0200
13.3 @@ -1,6 +1,6 @@
13.4 (* Title: Pure/ML-Systems/polyml_common.ML
13.5
13.6 -Compatibility file for Poly/ML -- common part for 4.x and 5.x.
13.7 +Compatibility file for Poly/ML -- common part for 5.x.
13.8 *)
13.9
13.10 exception Interrupt = SML90.Interrupt;
14.1 --- a/src/Pure/ML-Systems/polyml_old_basis.ML Sat May 30 22:37:38 2009 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,29 +0,0 @@
14.4 -(* Title: Pure/ML-Systems/polyml_old_basis.ML
14.5 -
14.6 -Fixes for the old SML basis library (before Poly/ML 4.2.0).
14.7 -*)
14.8 -
14.9 -structure String =
14.10 -struct
14.11 - fun isSuffix s1 s2 =
14.12 - let val n1 = size s1 and n2 = size s2
14.13 - in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
14.14 - fun isSubstring s1 s2 =
14.15 - String.isPrefix s1 s2 orelse
14.16 - size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE));
14.17 - open String;
14.18 -end;
14.19 -
14.20 -structure Substring =
14.21 -struct
14.22 - open Substring;
14.23 - val full = all;
14.24 -end;
14.25 -
14.26 -structure TextIO =
14.27 -struct
14.28 - open TextIO;
14.29 - fun inputLine is =
14.30 - let val s = TextIO.inputLine is
14.31 - in if s = "" then NONE else SOME s end;
14.32 -end;
15.1 --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML Sat May 30 22:37:38 2009 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,32 +0,0 @@
15.4 -(* Title: Pure/ML-Systems/polyml_old_compiler4.ML
15.5 -
15.6 -Runtime compilation -- for old PolyML.compiler (version 4.x).
15.7 -*)
15.8 -
15.9 -fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt =
15.10 - let
15.11 - val in_buffer = ref (explode (tune_source txt));
15.12 - val out_buffer = ref ([]: string list);
15.13 - fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
15.14 -
15.15 - fun get () =
15.16 - (case ! in_buffer of
15.17 - [] => ""
15.18 - | c :: cs => (in_buffer := cs; c));
15.19 - fun put s = out_buffer := s :: ! out_buffer;
15.20 -
15.21 - fun exec () =
15.22 - (case ! in_buffer of
15.23 - [] => ()
15.24 - | _ => (PolyML.compiler (get, put) (); exec ()));
15.25 - in
15.26 - exec () handle exn =>
15.27 - (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
15.28 - if verbose then print (output ()) else ()
15.29 - end;
15.30 -
15.31 -fun use_file context verbose name =
15.32 - let
15.33 - val instream = TextIO.openIn name;
15.34 - val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
15.35 - in use_text context (1, name) verbose txt end;