equal
deleted
inserted
replaced
19 |
19 |
20 ## prepare databases |
20 ## prepare databases |
21 |
21 |
22 if [ -z "$INFILE" ]; then |
22 if [ -z "$INFILE" ]; then |
23 INFILE="$ML_HOME/sml" |
23 INFILE="$ML_HOME/sml" |
24 EXIT="val exit = System.Unsafe.CInterface.exit;" |
24 EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;" |
25 else |
25 else |
26 EXIT="" |
26 EXIT="" |
27 fi |
27 fi |
28 |
28 |
29 MOVE="" |
29 MOVE="" |
30 |
30 |
31 if [ -z "$OUTFILE" ]; then |
31 if [ -z "$OUTFILE" ]; then |
32 COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\\n"); false);' |
32 COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);' |
33 else |
33 else |
34 if [ "$INFILE" -ef "$OUTFILE" ]; then |
34 if [ "$INFILE" -ef "$OUTFILE" ]; then |
35 OUTDIR=$(dirname "$OUTFILE")/tmp |
35 OUTDIR=$(dirname "$OUTFILE")/tmp |
36 OUTFILE=$OUTDIR/$(basename "$OUTFILE") |
36 OUTFILE=$OUTDIR/$(basename "$OUTFILE") |
37 mkdir -p "$OUTDIR" || fail_out |
37 mkdir -p "$OUTDIR" || fail_out |
39 fi |
39 fi |
40 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
40 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
41 COMMIT="fun commit () = not (exportML\"$OUTFILE\");" |
41 COMMIT="fun commit () = not (exportML\"$OUTFILE\");" |
42 fi |
42 fi |
43 |
43 |
|
44 |
|
45 ## run it! |
|
46 |
44 MLTEXT="$EXIT $COMMIT $MLTEXT" |
47 MLTEXT="$EXIT $COMMIT $MLTEXT" |
45 MLEXIT="commit();" |
48 MLEXIT="commit();" |
46 |
49 |
47 |
50 if [ -z "$TERMINATE" ]; then |
48 ## run it! |
51 FEEDER_OPTS="" |
49 |
|
50 START_SML="$INFILE $ML_OPTIONS" |
|
51 |
|
52 if [ -n "$TERMINATE" ]; then |
|
53 echo "$MLTEXT" "$MLEXIT" | $START_SML |
|
54 RC=$? |
|
55 elif [ -z "$MLTEXT" ]; then |
|
56 sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
|
57 RC=$? |
|
58 else |
52 else |
59 sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" |
53 FEEDER_OPTS="-q" |
60 RC=$? |
|
61 fi |
54 fi |
62 |
55 |
63 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
56 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
57 { read FPID; $INFILE $ML_OPTIONS; RC=$?; kill -HUP $FPID; exit $RC; } |
|
58 RC=$? |
|
59 |
|
60 |
|
61 ## fix heap file |
|
62 |
|
63 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
64 |
64 |
65 if [ -n "$MOVE" -a -f "$OUTFILE" ]; then |
65 if [ -n "$MOVE" -a -f "$OUTFILE" ]; then |
66 rm -f "$INFILE" || fail_out |
66 rm -f "$INFILE" || fail_out |
67 mv "$OUTFILE" "$INFILE" || fail_out |
67 mv "$OUTFILE" "$INFILE" || fail_out |
68 fi |
68 fi |