author | wenzelm |
Wed, 14 May 2008 11:05:10 +0200 | |
changeset 26882 | 9e824d8f4512 |
parent 26375 | 234f10289d97 |
child 29145 | b1c6f4563df7 |
permissions | -rwxr-xr-x |
21653 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# $Id$ |
|
4 |
# Author: Makarius |
|
5 |
# |
|
26213 | 6 |
# Poly/ML 5.0 startup script. |
21653 | 7 |
|
8 |
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
|
9 |
||
10 |
||
11 |
## diagnostics |
|
12 |
||
13 |
function fail_out() |
|
14 |
{ |
|
15 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
|
16 |
exit 2 |
|
17 |
} |
|
18 |
||
19 |
function check_file() |
|
20 |
{ |
|
21 |
if [ ! -f "$1" ]; then |
|
22 |
echo "Unable to locate $1" >&2 |
|
23 |
echo "Please check your ML system settings!" >&2 |
|
24 |
exit 2 |
|
25 |
fi |
|
26 |
} |
|
27 |
||
28 |
||
29 |
## compiler executables and libraries |
|
30 |
||
31 |
POLY="$ML_HOME/poly" |
|
32 |
check_file "$POLY" |
|
33 |
||
34 |
if [ "$(basename "$ML_HOME")" = bin ]; then |
|
35 |
POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)" |
|
36 |
else |
|
37 |
POLYLIB="$ML_HOME" |
|
38 |
fi |
|
39 |
||
40 |
export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH" |
|
41 |
export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH" |
|
42 |
||
43 |
||
44 |
## prepare databases |
|
45 |
||
46 |
if [ -z "$INFILE" ]; then |
|
21713
85722dc0fc81
more careful evaluation of ML text, prevents spurious output;
wenzelm
parents:
21711
diff
changeset
|
47 |
PRG="$POLY" |
21653 | 48 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
49 |
else |
|
50 |
check_file "$INFILE" |
|
21713
85722dc0fc81
more careful evaluation of ML text, prevents spurious output;
wenzelm
parents:
21711
diff
changeset
|
51 |
PRG="$INFILE" |
21653 | 52 |
EXIT="" |
53 |
fi |
|
54 |
||
55 |
if [ -z "$OUTFILE" ]; then |
|
56 |
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
|
57 |
else |
|
58 |
if [ -z "$COMPRESS" ]; then |
|
24296
3479a9fe73e0
removed signal setup from root function to on-entry hook;
wenzelm
parents:
22253
diff
changeset
|
59 |
COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
21653 | 60 |
else |
24296
3479a9fe73e0
removed signal setup from root function to on-entry hook;
wenzelm
parents:
22253
diff
changeset
|
61 |
COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
21653 | 62 |
fi |
63 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
64 |
rm -f "${OUTFILE}.o" || fail_out |
|
65 |
fi |
|
66 |
||
67 |
||
68 |
## run it! |
|
69 |
||
25124
a7dd8d3bf969
maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;
wenzelm
parents:
24480
diff
changeset
|
70 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
21653 | 71 |
MLEXIT="commit();" |
72 |
||
73 |
if [ -z "$TERMINATE" ]; then |
|
74 |
FEEDER_OPTS="" |
|
75 |
else |
|
76 |
FEEDER_OPTS="-q" |
|
77 |
fi |
|
78 |
||
26375
234f10289d97
back to feeder -- Isabelle ML setup no longer evaluates command line;
wenzelm
parents:
26213
diff
changeset
|
79 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
234f10289d97
back to feeder -- Isabelle ML setup no longer evaluates command line;
wenzelm
parents:
26213
diff
changeset
|
80 |
{ read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
21653 | 81 |
RC="$?" |
82 |
||
83 |
if [ -n "$OUTFILE" ]; then |
|
84 |
if [ -e "${OUTFILE}.o" ]; then |
|
24480
97c0ef49fa8f
renamed POLYML_LINK_OPTIONS to POLY_LINK_OPTIONS;
wenzelm
parents:
24479
diff
changeset
|
85 |
cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out |
21653 | 86 |
rm -f "${OUTFILE}.o" |
21711
dfac729d3066
root function: restore default interrupt handler;
wenzelm
parents:
21653
diff
changeset
|
87 |
[ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE" |
21653 | 88 |
fi |
89 |
[ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
90 |
fi |
|
91 |
||
92 |
exit "$RC" |