# HG changeset patch
# User wenzelm
# Date 1185216475 -7200
# Node ID 1b5f77bc146a2dbab8013ad11598902686ec992d
# Parent  079e99db59d78b5de4184f2de09aa070ae5af9ee
added compatibility wrapper for polyml-5.1;

diff -r 079e99db59d7 -r 1b5f77bc146a lib/scripts/run-polyml-5.1
--- /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"
diff -r 079e99db59d7 -r 1b5f77bc146a src/Pure/IsaMakefile
--- 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				\
diff -r 079e99db59d7 -r 1b5f77bc146a src/Pure/ML-Systems/polyml-5.1.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;