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): unit | exit _ = OS.Process.exit OS.Process.failure;" |
|
23 COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);" |
|
24 COMMIT_RO='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\\n"); false);' |
|
25 |
|
26 |
|
27 ## prepare databases |
20 ## prepare databases |
28 |
21 |
29 if [ -z "$INFILE" ]; then |
22 if [ -z "$INFILE" ]; then |
|
23 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
30 MLWORKS="mlworks-basis -tty" |
24 MLWORKS="mlworks-basis -tty" |
31 else |
25 else |
|
26 EXIT="" |
32 MLWORKS="mlimage -load $INFILE -tty" |
27 MLWORKS="mlimage -load $INFILE -tty" |
33 EXIT="" |
|
34 fi |
28 fi |
35 |
29 |
36 [ -z "$OUTFILE" ] && COMMIT="$COMMIT_RO" |
30 if [ -z "$OUTFILE" ]; then |
37 [ -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);' |
38 |
32 else |
39 MLTEXT="$EXIT $COMMIT $MLTEXT" |
33 COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);" |
40 MLEXIT="commit ();" |
34 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
35 fi |
41 |
36 |
42 |
37 |
43 ## run it! |
38 ## run it! |
44 |
39 |
45 START_MLWORKS="$ML_HOME/$MLWORKS 2>&1 $ML_OPTIONS" |
40 MLTEXT="$EXIT $COMMIT $MLTEXT" |
|
41 MLEXIT="commit();" |
46 |
42 |
47 if [ -n "$TERMINATE" ]; then |
43 if [ -z "$TERMINATE" ]; then |
48 sh -c "echo '$MLTEXT' '$MLEXIT' | $START_MLWORKS" |
44 FEEDER_OPTS="-s" |
49 RC=$? |
|
50 elif [ -z "$MLTEXT" ]; then |
|
51 sh -c "{ $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS" |
|
52 RC=$? |
|
53 else |
45 else |
54 sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS" |
46 FEEDER_OPTS="-q" |
55 RC=$? |
|
56 fi |
47 fi |
57 |
48 |
58 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
49 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
50 { read FPID; $ML_HOME/$MLWORKS $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; } |
|
51 RC=$? |
|
52 |
|
53 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
59 |
54 |
60 exit $RC |
55 exit $RC |