equal
deleted
inserted
replaced
|
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # MLWorks startup script (for 1.0r2 or later). |
|
6 # |
|
7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
|
8 # and from settings |
|
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 |
|
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 |
|
28 |
|
29 if [ -z "$INFILE" ]; then |
|
30 MLWORKS="mlworks-basis -tty" |
|
31 else |
|
32 MLWORKS="mlimage -load $INFILE -tty" |
|
33 EXIT="" |
|
34 fi |
|
35 |
|
36 [ -z "$OUTFILE" ] && COMMIT="$COMMIT_RO" |
|
37 [ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
38 |
|
39 MLTEXT="$EXIT $COMMIT $MLTEXT" |
|
40 MLEXIT="commit ();" |
|
41 |
|
42 |
|
43 ## run it! |
|
44 |
|
45 START_MLWORKS="$ML_HOME/$MLWORKS $ML_OPTIONS" |
|
46 |
|
47 if [ -n "$TERMINATE" ]; then |
|
48 sh -c "echo '$MLTEXT' '$MLEXIT' | $START_MLWORKS" |
|
49 RC=$? |
|
50 elif [ -z "$MLTEXT" ]; then |
|
51 sh -c "{ $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS" |
|
52 RC=$? |
|
53 else |
|
54 sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS" |
|
55 RC=$? |
|
56 fi |
|
57 |
|
58 #fix heap file name |
|
59 [ -n "$OUTFILE" -a -n "$SUFFIX" -a -f "$OUTFILE$SUFFIX" ] \ |
|
60 && mv "$OUTFILE$SUFFIX" "$OUTFILE" |
|
61 |
|
62 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
63 |
|
64 exit $RC |