--- a/lib/scripts/run-polyml-5.5.1 Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.5.1.
-
-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
-
-if [ -z "$INFILE" ]; then
- INIT=""
- EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
- check_file "$INFILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
- 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 \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
- 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: