--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.1 Mon Jul 23 20:47:55 2007 +0200
@@ -0,0 +1,99 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Makarius
+#
+# Poly/ML startup script (for 5.1)
+
+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
+ PRG="$POLY"
+ EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
+else
+ check_file "$INFILE"
+ PRG="$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
+
+if [ "$PRG" = "$POLY" ]; then
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+else
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+fi
+RC="$?"
+
+if [ -n "$OUTFILE" ]; then
+ if [ -e "${OUTFILE}.o" ]; then
+ cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml || 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/src/Pure/IsaMakefile Mon Jul 23 19:45:49 2007 +0200
+++ b/src/Pure/IsaMakefile Mon Jul 23 20:47:55 2007 +0200
@@ -41,13 +41,13 @@
Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML \
Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
ML-Systems/alice.ML ML-Systems/no_multithreading.ML \
- ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML \
- ML-Systems/polyml-5.0.ML ML-Systems/polyml-interrupt-timeout.ML \
- ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML \
- ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/smlnj.ML \
- Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
- Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy ROOT.ML \
- ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML \
+ ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML \
+ ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
+ ML-Systems/polyml-interrupt-timeout.ML ML-Systems/polyml-old-basis.ML \
+ ML-Systems/polyml-posix.ML ML-Systems/polyml.ML ML-Systems/poplogml.ML \
+ ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \
+ Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy \
+ ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML \
ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Mon Jul 23 20:47:55 2007 +0200
@@ -0,0 +1,41 @@
+(* Title: Pure/ML-Systems/polyml-5.0.ML
+ ID: $Id$
+
+Compatibility wrapper for Poly/ML 5.1.
+*)
+
+use "ML-Systems/polyml.ML";
+
+val pointer_eq = PolyML.pointerEq;
+
+
+(* improved versions of use_text/file *)
+
+fun use_text name (print, err) verbose txt =
+ let
+ val in_buffer = ref (explode txt);
+ val out_buffer = ref ([]: string list);
+ fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
+
+ val line_no = ref 1;
+ fun line () = ! line_no;
+ fun get () =
+ (case ! in_buffer of
+ [] => ""
+ | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
+ fun put s = out_buffer := s :: ! out_buffer;
+
+ fun exec () =
+ (case ! in_buffer of
+ [] => ()
+ | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
+ in
+ exec () handle exn => (err (output ()); raise exn);
+ if verbose then print (output ()) else ()
+ end;
+
+fun use_file output verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+ in use_text name output verbose txt end;