lib/scripts/run-polyml
author wenzelm
Thu Nov 13 23:45:15 2014 +0100 (2014-11-13)
changeset 58999 ed09ae4ea2d8
parent 56627 cb912b7de3cf
child 59344 e0ce214303c1
permissions -rwxr-xr-x
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2301
     2
#
wenzelm@26215
     3
# Author: Makarius
wenzelm@2314
     4
#
wenzelm@52831
     5
# Startup script for Poly/ML 5.1 ... 5.5.
wenzelm@9977
     6
wenzelm@31317
     7
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
wenzelm@2301
     8
wenzelm@2301
     9
wenzelm@2301
    10
## diagnostics
wenzelm@2301
    11
wenzelm@40544
    12
function fail()
wenzelm@40544
    13
{
wenzelm@40544
    14
  echo "$1" >&2
wenzelm@40544
    15
  exit 2
wenzelm@40544
    16
}
wenzelm@40544
    17
wenzelm@2349
    18
function fail_out()
wenzelm@2301
    19
{
wenzelm@40544
    20
  fail "Unable to create output heap file: \"$OUTFILE\""
wenzelm@2301
    21
}
wenzelm@2301
    22
wenzelm@10206
    23
function check_file()
wenzelm@5063
    24
{
wenzelm@40544
    25
  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
wenzelm@5063
    26
}
wenzelm@5063
    27
wenzelm@2301
    28
wenzelm@26215
    29
## compiler executables and libraries
wenzelm@16374
    30
wenzelm@40544
    31
[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
wenzelm@40544
    32
wenzelm@21356
    33
POLY="$ML_HOME/poly"
wenzelm@10206
    34
check_file "$POLY"
wenzelm@2301
    35
wenzelm@52831
    36
librarypath "$ML_HOME"
wenzelm@10206
    37
wenzelm@9765
    38
wenzelm@9765
    39
wenzelm@2301
    40
## prepare databases
wenzelm@2301
    41
wenzelm@2301
    42
if [ -z "$INFILE" ]; then
wenzelm@26215
    43
  INIT=""
wenzelm@56627
    44
  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
wenzelm@10105
    45
else
wenzelm@26215
    46
  check_file "$INFILE"
wenzelm@51099
    47
  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));"
wenzelm@26215
    48
  EXIT=""
wenzelm@2301
    49
fi
wenzelm@2301
    50
wenzelm@2301
    51
if [ -z "$OUTFILE" ]; then
wenzelm@39619
    52
  COMMIT='fun commit () = false;'
wenzelm@39619
    53
  MLEXIT=""
wenzelm@2301
    54
else
wenzelm@53657
    55
  if [ -z "$INFILE" ]; then
wenzelm@53657
    56
    COMMIT="fun commit () = (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);"
wenzelm@53657
    57
  else
wenzelm@53657
    58
    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
wenzelm@53657
    59
  fi
wenzelm@26215
    60
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@39619
    61
  MLEXIT="commit();"
wenzelm@2301
    62
fi
wenzelm@2301
    63
wenzelm@2301
    64
wenzelm@2301
    65
## run it!
wenzelm@2301
    66
wenzelm@26215
    67
MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
wenzelm@26215
    68
wenzelm@16254
    69
if [ -z "$TERMINATE" ]; then
wenzelm@16254
    70
  FEEDER_OPTS=""
wenzelm@16254
    71
else
wenzelm@16254
    72
  FEEDER_OPTS="-q"
wenzelm@16254
    73
fi
wenzelm@16254
    74
wenzelm@26215
    75
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@48002
    76
  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
wenzelm@9789
    77
RC="$?"
wenzelm@2301
    78
wenzelm@4505
    79
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@2301
    80
wenzelm@9789
    81
exit "$RC"
wenzelm@40480
    82
wenzelm@40480
    83
#:wrap=soft:maxLineLen=100: