equal
deleted
inserted
replaced
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 TERMINATE, |
7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE, |
8 # and from settings |
8 # and from settings |
9 |
9 |
10 |
10 |
11 ## diagnostics |
11 ## diagnostics |
12 |
12 |
29 esac |
29 esac |
30 |
30 |
31 |
31 |
32 ## prepare databases |
32 ## prepare databases |
33 |
33 |
34 MLINIT="" |
34 COPYDB=true |
35 |
35 |
36 if [ -z "$INFILE" ]; then |
36 if [ -z "$INFILE" ]; then |
37 INFILE="$ML_HOME/ML_dbase" |
37 INFILE="$ML_HOME/ML_dbase" |
38 MLINIT="val use = PolyML.use; val exit = PolyML.exit; fun init_database () = ();" |
38 MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT" |
|
39 COPYDB="" |
39 fi |
40 fi |
40 |
41 |
41 if [ -z "$OUTFILE" ]; then |
42 if [ -z "$OUTFILE" ]; then |
42 DB="$INFILE" |
43 DB="$INFILE" |
43 ML_OPTIONS="-r $ML_OPTIONS" |
44 ML_OPTIONS="-r $ML_OPTIONS" |
51 else |
52 else |
52 [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
53 [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
53 echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE" |
54 echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE" |
54 [ -f "$OUTFILE" ] || fail_out |
55 [ -f "$OUTFILE" ] || fail_out |
55 DB="$OUTFILE" |
56 DB="$OUTFILE" |
56 MLINIT="$MLINIT init_database ();" |
|
57 fi |
57 fi |
58 |
58 |
59 |
59 |
60 ## run it! |
60 ## run it! |
61 |
61 |
62 START_POLY="$POLY $ML_OPTIONS $DB" |
62 START_POLY="$POLY $ML_OPTIONS $DB" |
63 DB_INFO=$(ls -l "$DB") |
63 DB_INFO=$(ls -l "$DB") |
64 |
|
65 [ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT" |
|
66 |
64 |
67 if [ -n "$TERMINATE" ]; then |
65 if [ -n "$TERMINATE" ]; then |
68 echo "$MLTEXT" | $START_POLY |
66 echo "$MLTEXT" | $START_POLY |
69 RC=$? |
67 RC=$? |
70 elif [ -z "$MLTEXT" ]; then |
68 elif [ -z "$MLTEXT" ]; then |