# HG changeset patch
# User wenzelm
# Date 1212011083 -7200
# Node ID 12795abea6b69c8bef6b74402ec8e0849250f413
# Parent  e6229d8d6aaa59e0032e0990da5f1a65d2e8ff8a
obsolete;

diff -r e6229d8d6aaa -r 12795abea6b6 Admin/Isabelle2005-polyml-5.0/README-polyml-5.0
--- 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$
diff -r e6229d8d6aaa -r 12795abea6b6 Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0
--- 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"
diff -r e6229d8d6aaa -r 12795abea6b6 Admin/Isabelle2005-polyml-5.0/src/Pure/ML-Systems/polyml-5.0.ML
--- 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;
diff -r e6229d8d6aaa -r 12795abea6b6 Admin/polyml-5.1/README
--- 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$