equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
|
2 # :mode=shellscript: |
|
3 # |
|
4 # Author: Makarius |
|
5 # |
|
6 # Startup script for Poly/ML 5.6. |
|
7 |
|
8 export -n HEAP_FILE ML_TEXT TERMINATE |
|
9 |
|
10 |
|
11 ## diagnostics |
|
12 |
|
13 function fail() |
|
14 { |
|
15 echo "$1" >&2 |
|
16 exit 2 |
|
17 } |
|
18 |
|
19 function check_file() |
|
20 { |
|
21 [ ! -f "$1" ] && fail "Unable to locate \"$1\"" |
|
22 } |
|
23 |
|
24 |
|
25 ## heap file |
|
26 |
|
27 if [ -z "$HEAP_FILE" ]; then |
|
28 case "$ML_PLATFORM" in |
|
29 *-windows) |
|
30 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));" |
|
31 ;; |
|
32 *) |
|
33 INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);" |
|
34 ;; |
|
35 esac |
|
36 else |
|
37 check_file "$HEAP_FILE" |
|
38 case "$ML_PLATFORM" in |
|
39 *-windows) |
|
40 PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")" |
|
41 ;; |
|
42 *) |
|
43 PLATFORM_HEAP_FILE="$HEAP_FILE" |
|
44 ;; |
|
45 esac |
|
46 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);" |
|
47 fi |
|
48 |
|
49 |
|
50 ## poly process |
|
51 |
|
52 ML_TEXT="$INIT $ML_TEXT" |
|
53 |
|
54 check_file "$ML_HOME/poly" |
|
55 librarypath "$ML_HOME" |
|
56 |
|
57 if [ -n "$TERMINATE" ]; then |
|
58 "$ML_HOME/poly" -q -i $ML_OPTIONS \ |
|
59 --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$ML_TEXT")" \ |
|
60 --error-exit </dev/null |
|
61 RC="$?" |
|
62 else |
|
63 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" | \ |
|
64 { read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
|
65 RC="$?" |
|
66 fi |
|
67 |
|
68 exit "$RC" |
|
69 |
|
70 #:wrap=soft:maxLineLen=100: |
|