lib/scripts/run-polyml

isabelle_process executable no longer supports writable heap images;

#!/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="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); 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: