--- a/Admin/Isabelle2005-polyml-5.0/README-polyml-5.0 Wed May 28 23:43:39 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-
-Using Isabelle2005 with Poly/ML 5.0 requires the following
-compatibility wrappers:
-
- Isabelle2005/src/Pure/ML-Systems/polyml-5.0.ML
- Isabelle2005/lib/scripts/run-polyml-5.0
-
-The Isabelle settings need to specify that version, by including
-something like this in Isabelle2005/etc/settings or
-~/isabelle/etc/settings:
-
- ML_PLATFORM=""
- ML_HOME=/usr/local/bin
- ML_SYSTEM=polyml-5.0
- ML_OPTIONS="-H 500"
-
-Now logics can be compiled as usual, cf. the INSTALL instructions.
-
-
-ProofGeneral needs to be adapted as well, by including the following
-in Isabelle2005/etc/proofgeneral-settings.el or
-~/isabelle/etc/proofgeneral-settings.el:
-
- (custom-set-variables
- '(proof-shell-pre-interrupt-hook (lambda () t)))
-
-Otherwise ProofGeneral will regard polyml-5.0 as an old polyml-3.x and
-activate strange workarounds for interrupt handling.
-
-
- Makarius
- 11-Dec-2006
-
-$Id$
--- a/Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0 Wed May 28 23:43:39 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Makarius
-#
-# Poly/ML startup script (for 5.0)
-
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
-}
-
-function check_file()
-{
- if [ ! -f "$1" ]; then
- echo "Unable to locate $1" >&2
- echo "Please check your ML system settings!" >&2
- exit 2
- fi
-}
-
-
-## compiler executables and libraries
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-if [ "$(basename "$ML_HOME")" = bin ]; then
- POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
-else
- POLYLIB="$ML_HOME"
-fi
-
-export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
-export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
-else
- check_file "$INFILE"
- POLY="$INFILE"
- EXIT=""
-fi
-
-ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
-
-if [ -z "$OUTFILE" ]; then
- COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
-else
- if [ -z "$COMPRESS" ]; then
- COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
- else
- COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
- fi
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
- rm -f "${OUTFILE}.o" || fail_out
-fi
-
-
-## run it!
-
-MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-if [ -n "$OUTFILE" ]; then
- if [ -e "${OUTFILE}.o" ]; then
- cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
- rm -f "${OUTFILE}.o"
- [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
- fi
- [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-fi
-
-exit "$RC"
--- a/Admin/Isabelle2005-polyml-5.0/src/Pure/ML-Systems/polyml-5.0.ML Wed May 28 23:43:39 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.0.ML
- ID: $Id$
-
-Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005.
-*)
-
-structure Posix =
-struct
- open Posix;
- structure IO =
- struct
- open IO;
- val mkReader = mkTextReader;
- val mkWriter = mkTextWriter;
- end;
-end;
-
-structure TextIO =
-struct
- open TextIO;
- fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
-end;
-
-structure Substring =
-struct
- open Substring;
- val all = full;
-end;
-
-
-use "ML-Systems/polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
--- a/Admin/polyml-5.1/README Wed May 28 23:43:39 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-
-This distribution of Poly/ML 5.1 has been compiled from the original
-sources (available from http://sourceforge.net/projects/polyml/) as
-follows:
-
- tar xvzf polyml.5.1.tar.gz
- cd polyml.5.1
- ./configure --prefix=/tmp/polyml --without-x
- make
- make install
-
-Now /tmp/polyml/bin/* and /tmp/polyml/lib/* are moved to the
-platform-specific target directory (e.g. polyml-5.1/x86-linux). Note
-that the script Isabelle/lib/scripts/polyml-platform identifies your
-platform.
-
-
- Makarius
- 22-Nov-2007
-
-$Id$