--- a/lib/scripts/run-polyml Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.6.
-
-export -n HEAP_FILE ML_TEXT TERMINATE
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function check_file()
-{
- [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## heap file
-
-if [ -z "$HEAP_FILE" ]; then
- case "$ML_PLATFORM" in
- *-windows)
- INIT="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));"
- ;;
- *)
- INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
- ;;
- esac
-else
- check_file "$HEAP_FILE"
- case "$ML_PLATFORM" in
- *-windows)
- PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
- ;;
- *)
- PLATFORM_HEAP_FILE="$HEAP_FILE"
- ;;
- esac
- INIT="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success);"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -n "$TERMINATE" ]; then
- "$ML_HOME/poly" -q -i $ML_OPTIONS \
- --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$ML_TEXT")" \
- --error-exit </dev/null
- RC="$?"
-else
- "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" | \
- { read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
- RC="$?"
-fi
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100: