1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Markus Wenzel, TU Muenchen |
|
4 # |
|
5 # SML/NJ startup script (for 110 or later). |
|
6 |
|
7 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE |
|
8 |
|
9 |
|
10 ## diagnostics |
|
11 |
|
12 function fail() |
|
13 { |
|
14 echo "$1" >&2 |
|
15 exit 2 |
|
16 } |
|
17 |
|
18 function fail_out() |
|
19 { |
|
20 fail "Unable to create output heap file: \"$OUTFILE\"" |
|
21 } |
|
22 |
|
23 function check_mlhome_file() |
|
24 { |
|
25 [ ! -f "$1" ] && fail "Unable to locate \"$1\"" |
|
26 } |
|
27 |
|
28 function check_heap_file() |
|
29 { |
|
30 if [ ! -f "$1" ]; then |
|
31 echo "Expected to find ML heap file $1" >&2 |
|
32 return 1 |
|
33 else |
|
34 return 0 |
|
35 fi |
|
36 } |
|
37 |
|
38 |
|
39 |
|
40 ## compiler binaries |
|
41 |
|
42 [ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)" |
|
43 |
|
44 SML="$ML_HOME/sml" |
|
45 ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys" |
|
46 |
|
47 check_mlhome_file "$SML" |
|
48 check_mlhome_file "$ARCH_N_OPSYS" |
|
49 |
|
50 eval $("$ARCH_N_OPSYS") |
|
51 |
|
52 |
|
53 |
|
54 ## prepare databases |
|
55 |
|
56 if [ -z "$INFILE" ]; then |
|
57 EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);" |
|
58 DB="" |
|
59 else |
|
60 EXIT="" |
|
61 DB="@SMLload=$INFILE" |
|
62 fi |
|
63 |
|
64 if [ -z "$OUTFILE" ]; then |
|
65 MLEXIT="" |
|
66 else |
|
67 if [ -z "$INFILE" ]; then |
|
68 MLEXIT="if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};" |
|
69 else |
|
70 MLEXIT="Session.save \"$OUTFILE\";" |
|
71 fi |
|
72 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
|
73 fi |
|
74 |
|
75 |
|
76 ## run it! |
|
77 |
|
78 MLTEXT="$EXIT $MLTEXT" |
|
79 |
|
80 if [ -z "$TERMINATE" ]; then |
|
81 FEEDER_OPTS="" |
|
82 else |
|
83 FEEDER_OPTS="-q" |
|
84 fi |
|
85 |
|
86 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
|
87 { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; } |
|
88 RC="$?" |
|
89 |
|
90 |
|
91 ## fix heap file name and permissions |
|
92 |
|
93 if [ -n "$OUTFILE" ]; then |
|
94 check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
|
95 fi |
|
96 |
|
97 exit "$RC" |
|