15 echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
15 echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
16 exit 2 |
16 exit 2 |
17 } |
17 } |
18 |
18 |
19 |
19 |
20 ## basic setup |
|
21 |
|
22 EXIT="fun exit 0 : unit = OS.Process.exit OS.Process.success | exit _ = OS.Process.exit OS.Process.failure;" |
|
23 COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");" |
|
24 COMMIT_RO='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\\n"); false);' |
|
25 eval $($ML_HOME/.arch-n-opsys) |
|
26 SUFFIX=".$ARCH-$OPSYS" |
|
27 |
|
28 |
|
29 ## prepare databases |
20 ## prepare databases |
30 |
21 |
31 DB="$INFILE" |
22 if [ -z "$INFILE" ]; then |
32 |
23 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
33 if [ -n "$DB" ]; then |
24 DB="" |
|
25 else |
|
26 EXIT="" |
34 DB="@SMLload=$INFILE" |
27 DB="@SMLload=$INFILE" |
35 EXIT="" |
|
36 fi |
28 fi |
37 |
29 |
38 [ -z "$OUTFILE" ] && COMMIT="$COMMIT_RO" |
30 if [ -z "$OUTFILE" ]; then |
39 [ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
31 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
40 |
32 else |
41 MLTEXT="$EXIT $COMMIT $MLTEXT" |
33 COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");" |
42 MLEXIT="commit ();" |
34 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
35 fi |
43 |
36 |
44 |
37 |
45 ## run it! |
38 ## run it! |
46 |
39 |
47 START_SML="$ML_HOME/sml $ML_OPTIONS $DB" |
40 MLTEXT="$EXIT $COMMIT $MLTEXT" |
|
41 MLEXIT="commit();" |
48 |
42 |
49 if [ -n "$TERMINATE" ]; then |
43 if [ -z "$TERMINATE" ]; then |
50 sh -c "echo '$MLTEXT' '$MLEXIT' | $START_SML" |
44 FEEDER_OPTS="" |
51 RC=$? |
|
52 elif [ -z "$MLTEXT" ]; then |
|
53 sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
|
54 RC=$? |
|
55 else |
45 else |
56 sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
46 FEEDER_OPTS="-q" |
57 RC=$? |
|
58 fi |
47 fi |
59 |
48 |
60 #fix heap file name |
49 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
61 [ -n "$OUTFILE" -a -n "$SUFFIX" -a -f "$OUTFILE$SUFFIX" ] \ |
50 { read FPID; $ML_HOME/sml $ML_OPTIONS $DB; RC=$?; kill -HUP $FPID; exit $RC; } |
62 && mv "$OUTFILE$SUFFIX" "$OUTFILE" |
51 RC=$? |
63 |
52 |
64 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
53 |
|
54 ## fix heap file name and permissions |
|
55 |
|
56 if [ -n "$OUTFILE" ]; then |
|
57 eval $($ML_HOME/.arch-n-opsys) |
|
58 SUFFIX=".$ARCH-$OPSYS" |
|
59 if [ -f "$OUTFILE$SUFFIX" ]; then |
|
60 mv "$OUTFILE$SUFFIX" "$OUTFILE" |
|
61 [ -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
62 fi |
|
63 fi |
65 |
64 |
66 exit $RC |
65 exit $RC |