lib/scripts/run-polyml-5.5.3

--- a/lib/scripts/run-polyml-5.5.3	Sun Dec 06 17:27:42 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.5.3.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function fail_out()
-{
-  fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
-
-case "$ML_PLATFORM" in
-  *-windows)
-    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
-    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
-    ;;
-  *)
-    PLATFORM_INFILE="$INFILE"
-    PLATFORM_OUTFILE="$OUTFILE"
-    ;;
-esac
-
-if [ -z "$INFILE" ]; then
-  INIT=""
-  case "$ML_PLATFORM" in
-    *-windows)
-      EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
-      ;;
-    *)
-      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-      ;;
-  esac
-else
-  check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
-  EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
-  MLEXIT=""
-else
-  if [ -z "$INFILE" ]; then
-    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
-  else
-    MLEXIT="Session.save \"$OUTFILE\";"
-  fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$INIT $EXIT $MLTEXT"
-
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
-  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
-    --error-exit </dev/null
-  RC="$?"
-else
-  if [ -z "$TERMINATE" ]; then
-    FEEDER_OPTS=""
-  else
-    FEEDER_OPTS="-q"
-    ML_OPTIONS="$ML_OPTIONS --error-exit"
-  fi
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-  RC="$?"
-fi
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100: