removed obsolete support for polyml-4.9.1;
authorwenzelm
Sat Dec 30 12:41:59 2006 +0100 (2006-12-30)
changeset 219618d34e64eeaf6
parent 21960 0574f192b78a
child 21962 279b129498b6
removed obsolete support for polyml-4.9.1;
lib/scripts/run-polyml-4.9.1
src/Pure/IsaMakefile
src/Pure/ML-Systems/polyml-4.9.1.ML
     1.1 --- a/lib/scripts/run-polyml-4.9.1	Sat Dec 30 12:38:51 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,90 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# $Id$
     1.7 -# Author: Makarius
     1.8 -#
     1.9 -# Poly/ML startup script (for 4.9.1)
    1.10 -
    1.11 -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
    1.12 -
    1.13 -
    1.14 -## diagnostics
    1.15 -
    1.16 -function fail_out()
    1.17 -{
    1.18 -  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
    1.19 -  exit 2
    1.20 -}
    1.21 -
    1.22 -function check_file()
    1.23 -{
    1.24 -  if [ ! -f "$1" ]; then
    1.25 -    echo "Unable to locate $1" >&2
    1.26 -    echo "Please check your ML system settings!" >&2
    1.27 -    exit 2
    1.28 -  fi
    1.29 -}
    1.30 -
    1.31 -
    1.32 -## compiler executables and libraries
    1.33 -
    1.34 -POLY="$ML_HOME/poly"
    1.35 -check_file "$POLY"
    1.36 -
    1.37 -if [ "$(basename "$ML_HOME")" = bin ]; then
    1.38 -  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
    1.39 -else
    1.40 -  POLYLIB="$ML_HOME"
    1.41 -fi
    1.42 -
    1.43 -export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
    1.44 -export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
    1.45 -
    1.46 -
    1.47 -## prepare databases
    1.48 -
    1.49 -if [ -z "$INFILE" ]; then
    1.50 -  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    1.51 -else
    1.52 -  check_file "$INFILE"
    1.53 -  POLY="$INFILE"
    1.54 -  EXIT=""
    1.55 -fi
    1.56 -
    1.57 -if [ -z "$OUTFILE" ]; then
    1.58 -  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    1.59 -else
    1.60 -  if [ -z "$COMPRESS" ]; then
    1.61 -    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    1.62 -  else
    1.63 -    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    1.64 -  fi
    1.65 -  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    1.66 -  rm -f "${OUTFILE}.o" || fail_out
    1.67 -fi
    1.68 -
    1.69 -
    1.70 -## run it!
    1.71 -
    1.72 -MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
    1.73 -MLEXIT="commit();"
    1.74 -
    1.75 -if [ -z "$TERMINATE" ]; then
    1.76 -  FEEDER_OPTS=""
    1.77 -else
    1.78 -  FEEDER_OPTS="-q"
    1.79 -fi
    1.80 -
    1.81 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    1.82 -  { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.83 -RC="$?"
    1.84 -
    1.85 -if [ -n "$OUTFILE" ]; then
    1.86 -  if [ -e "${OUTFILE}.o" ]; then
    1.87 -    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
    1.88 -    rm -f "${OUTFILE}.o"
    1.89 -  fi
    1.90 -  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    1.91 -fi
    1.92 -
    1.93 -exit "$RC"
     2.1 --- a/src/Pure/IsaMakefile	Sat Dec 30 12:38:51 2006 +0100
     2.2 +++ b/src/Pure/IsaMakefile	Sat Dec 30 12:41:59 2006 +0100
     2.3 @@ -43,12 +43,11 @@
     2.4    Isar/session.ML Isar/skip_proof.ML Isar/specification.ML			\
     2.5    Isar/term_style.ML Isar/theory_target.ML Isar/thy_header.ML Isar/toplevel.ML	\
     2.6    ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML			\
     2.7 -  ML-Systems/polyml-4.9.1.ML ML-Systems/polyml-5.0.ML 				\
     2.8 -  ML-Systems/polyml-interrupt-timeout.ML ML-Systems/polyml-posix.ML		\
     2.9 -  ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/smlnj.ML		\
    2.10 -  Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML	\
    2.11 -  Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy ROOT.ML			\
    2.12 -  ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML 				\
    2.13 +  ML-Systems/polyml-5.0.ML ML-Systems/polyml-interrupt-timeout.ML		\
    2.14 +  ML-Systems/polyml-posix.ML ML-Systems/polyml.ML ML-Systems/poplogml.ML	\
    2.15 +  ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML		\
    2.16 +  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy	\
    2.17 +  ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML			\
    2.18    ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML                     \
    2.19    ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML ProofGeneral/pgip_tests.ML	\
    2.20    ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML			\
     3.1 --- a/src/Pure/ML-Systems/polyml-4.9.1.ML	Sat Dec 30 12:38:51 2006 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,10 +0,0 @@
     3.4 -(*  Title:      Pure/ML-Systems/polyml-4.9.1.ML
     3.5 -    ID:         $Id$
     3.6 -
     3.7 -Compatibility wrapper for Poly/ML 4.9.1.
     3.8 -*)
     3.9 -
    3.10 -use "ML-Systems/polyml-4.1.4-patch.ML";
    3.11 -use "ML-Systems/polyml.ML";
    3.12 -
    3.13 -val pointer_eq = PolyML.pointerEq;