added compatibility wrapper for polyml-5.1;
authorwenzelm
Mon Jul 23 20:47:55 2007 +0200 (2007-07-23)
changeset 239431b5f77bc146a
parent 23942 079e99db59d7
child 23944 2ea068548a83
added compatibility wrapper for polyml-5.1;
lib/scripts/run-polyml-5.1
src/Pure/IsaMakefile
src/Pure/ML-Systems/polyml-5.1.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/scripts/run-polyml-5.1	Mon Jul 23 20:47:55 2007 +0200
     1.3 @@ -0,0 +1,99 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +# Author: Makarius
     1.8 +#
     1.9 +# Poly/ML startup script (for 5.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 +  PRG="$POLY"
    1.51 +  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    1.52 +else
    1.53 +  check_file "$INFILE"
    1.54 +  PRG="$INFILE"
    1.55 +  EXIT=""
    1.56 +fi
    1.57 +
    1.58 +ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
    1.59 +
    1.60 +if [ -z "$OUTFILE" ]; then
    1.61 +  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    1.62 +else
    1.63 +  if [ -z "$COMPRESS" ]; then
    1.64 +    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
    1.65 +  else
    1.66 +    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
    1.67 +  fi
    1.68 +  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    1.69 +  rm -f "${OUTFILE}.o" || fail_out
    1.70 +fi
    1.71 +
    1.72 +
    1.73 +## run it!
    1.74 +
    1.75 +MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
    1.76 +MLEXIT="commit();"
    1.77 +
    1.78 +if [ -z "$TERMINATE" ]; then
    1.79 +  FEEDER_OPTS=""
    1.80 +else
    1.81 +  FEEDER_OPTS="-q"
    1.82 +fi
    1.83 +
    1.84 +if [ "$PRG" = "$POLY" ]; then
    1.85 +  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    1.86 +    { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.87 +else
    1.88 +  "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
    1.89 +    { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.90 +fi
    1.91 +RC="$?"
    1.92 +
    1.93 +if [ -n "$OUTFILE" ]; then
    1.94 +  if [ -e "${OUTFILE}.o" ]; then
    1.95 +    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml || fail_out
    1.96 +    rm -f "${OUTFILE}.o"
    1.97 +    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
    1.98 +  fi
    1.99 +  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   1.100 +fi
   1.101 +
   1.102 +exit "$RC"
     2.1 --- a/src/Pure/IsaMakefile	Mon Jul 23 19:45:49 2007 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Mon Jul 23 20:47:55 2007 +0200
     2.3 @@ -41,13 +41,13 @@
     2.4    Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML	\
     2.5    Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML			\
     2.6    ML-Systems/alice.ML ML-Systems/no_multithreading.ML 				\
     2.7 -  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML				\
     2.8 -  ML-Systems/polyml-5.0.ML ML-Systems/polyml-interrupt-timeout.ML		\
     2.9 -  ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML 			\
    2.10 -  ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/smlnj.ML		\
    2.11 -  Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML	\
    2.12 -  Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy ROOT.ML			\
    2.13 -  ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML 				\
    2.14 +  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML 			\
    2.15 +  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML				\
    2.16 +  ML-Systems/polyml-interrupt-timeout.ML ML-Systems/polyml-old-basis.ML		\
    2.17 +  ML-Systems/polyml-posix.ML ML-Systems/polyml.ML ML-Systems/poplogml.ML	\
    2.18 +  ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML		\
    2.19 +  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy	\
    2.20 +  ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML			\
    2.21    ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML			\
    2.22    ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML	\
    2.23    ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML				\
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Mon Jul 23 20:47:55 2007 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(*  Title:      Pure/ML-Systems/polyml-5.0.ML
     3.5 +    ID:         $Id$
     3.6 +
     3.7 +Compatibility wrapper for Poly/ML 5.1.
     3.8 +*)
     3.9 +
    3.10 +use "ML-Systems/polyml.ML";
    3.11 +
    3.12 +val pointer_eq = PolyML.pointerEq;
    3.13 +
    3.14 +
    3.15 +(* improved versions of use_text/file *)
    3.16 +
    3.17 +fun use_text name (print, err) verbose txt =
    3.18 +  let
    3.19 +    val in_buffer = ref (explode txt);
    3.20 +    val out_buffer = ref ([]: string list);
    3.21 +    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    3.22 +
    3.23 +    val line_no = ref 1;
    3.24 +    fun line () = ! line_no;
    3.25 +    fun get () =
    3.26 +      (case ! in_buffer of
    3.27 +        [] => ""
    3.28 +      | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
    3.29 +    fun put s = out_buffer := s :: ! out_buffer;
    3.30 +
    3.31 +    fun exec () =
    3.32 +      (case ! in_buffer of
    3.33 +        [] => ()
    3.34 +      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
    3.35 +  in
    3.36 +    exec () handle exn => (err (output ()); raise exn);
    3.37 +    if verbose then print (output ()) else ()
    3.38 +  end;
    3.39 +
    3.40 +fun use_file output verbose name =
    3.41 +  let
    3.42 +    val instream = TextIO.openIn name;
    3.43 +    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    3.44 +  in use_text name output verbose txt end;