1 #!/bin/bash |
1 #!/bin/bash -norc |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # Poly/ML startup script. |
5 # Poly/ML startup script. |
6 # |
6 # |
7 # Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE, |
7 # Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE, |
8 # and from settings |
8 # and from settings |
9 |
9 |
10 |
10 |
11 ## diagnostics |
11 ## diagnostics |
12 |
12 |
13 function fail() |
13 function fail_out() |
14 { |
14 { |
15 echo "$1" |
15 echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
16 exit 2 |
16 exit 2 |
17 } |
17 } |
18 |
18 |
19 |
19 |
20 |
|
21 ## locations and settings |
20 ## locations and settings |
22 |
21 |
23 ML_QUIT=";PolyML.quit();" |
|
24 ML_DBASE=$ML_HOME/ML_dbase |
22 ML_DBASE=$ML_HOME/ML_dbase |
25 POLY=$ML_HOME/poly |
23 POLY=$ML_HOME/poly |
26 DISCGARB=$ML_HOME/discgarb |
24 DISCGARB=$ML_HOME/discgarb |
27 |
25 |
28 case "$ML_SYSTEM" in |
26 case "$ML_SYSTEM" in |
29 polyml-3.1) |
27 polyml-3.*) |
30 DISCGARB="$DISCGARB -c" |
28 DISCGARB="$DISCGARB -c" |
31 export LM_LICENSE_FILE=$ML_HOME/license.dat |
|
32 ;; |
29 ;; |
33 esac |
30 esac |
34 |
31 |
35 |
32 |
|
33 ## prepare databases |
36 |
34 |
37 ## prepare databases |
35 MLINIT="" |
38 |
36 |
39 if [ -z "$INFILE" ]; then |
37 if [ -z "$INFILE" ]; then |
40 INFILE="$ML_DBASE" |
38 INFILE="$ML_DBASE" |
41 MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT" |
39 MLINIT="val use = PolyML.use; val exit = PolyML.exit; fun init_database () = ();" |
42 fi |
40 fi |
43 |
|
44 function fail_out() |
|
45 { |
|
46 fail "Unable to create output heap file: \"$OUTFILE\"" |
|
47 } |
|
48 |
41 |
49 if [ -z "$OUTFILE" ]; then |
42 if [ -z "$OUTFILE" ]; then |
50 DB="$INFILE" |
43 DB="$INFILE" |
51 OPTS="-r" |
44 ML_OPTIONS="-r $ML_OPTIONS" |
52 elif [ "$INFILE" = "$OUTFILE" ]; then # FIXME -ef !? |
45 elif [ "$INFILE" -ef "$OUTFILE" ]; then |
53 DB="$INFILE" |
46 DB="$INFILE" |
54 OPTS="" |
|
55 elif [ -n "$COPYDB" ]; then |
47 elif [ -n "$COPYDB" ]; then |
56 cp "$INFILE" "$OUTFILE" || fail_out |
48 cp "$INFILE" "$OUTFILE" || fail_out |
57 chmod +w "$OUTFILE" |
49 chmod +w "$OUTFILE" || fail_out |
58 DB="$OUTFILE" |
50 DB="$OUTFILE" |
59 OPTS="" |
|
60 else |
51 else |
61 [ -f "$OUTFILE" ] && { rm "$OUTFILE" || fail_out } |
52 [ -f "$OUTFILE" ] && { rm "$OUTFILE" || fail_out } |
62 echo "PolyML.make_database \"$OUTFILE\"; $ML_QUIT" | $POLY -r "$INFILE" |
53 echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE" |
63 [ -f "$OUTFILE" ] || fail_out |
54 [ -f "$OUTFILE" ] || fail_out |
64 DB="$OUTFILE" |
55 DB="$OUTFILE" |
65 OPTS="" |
56 MLINIT="$MLINIT init_database ();" |
66 fi |
57 fi |
67 |
|
68 |
58 |
69 |
59 |
70 ## run it! |
60 ## run it! |
71 |
61 |
72 START_POLY="$POLY $OPTS $ML_OPTIONS $OPTIONS $DB" |
62 START_POLY="$POLY $ML_OPTIONS $DB" |
|
63 |
|
64 [ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT" |
73 |
65 |
74 if [ -n "$TERMINATE" ]; then |
66 if [ -n "$TERMINATE" ]; then |
75 echo "$MLTEXT" "$ML_QUIT" | $START_POLY |
67 echo "$MLTEXT" | $START_POLY |
76 RC=$? |
68 RC=$? |
77 elif [ -z "$MLTEXT" ]; then |
69 elif [ -z "$MLTEXT" ]; then |
78 $START_POLY |
70 $START_POLY |
79 RC=$? |
71 RC=$? |
80 else |
72 else |
81 TMP_FILE=/tmp/mltext-$$ |
73 { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat } | $START_POLY |
82 echo "$MLTEXT" >$TMP_FILE |
|
83 $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_POLY |
|
84 RC=$? |
74 RC=$? |
85 rm $TMP_FILE |
|
86 fi |
75 fi |
87 |
76 |
88 [ $RC -eq 0 -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE" |
77 [ $RC -eq 0 -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE" |
89 |
78 |
90 exit $RC |
79 exit $RC |