equal
deleted
inserted
replaced
26 } |
26 } |
27 |
27 |
28 |
28 |
29 ## Poly/ML programs |
29 ## Poly/ML programs |
30 |
30 |
|
31 FEEDER="" |
31 ML_DBASE_PREFIX="" |
32 ML_DBASE_PREFIX="" |
32 POLY="$ML_HOME/poly" |
33 POLY="$ML_HOME/poly" |
33 check_file "$POLY" |
34 check_file "$POLY" |
34 |
35 |
35 case "$ML_SYSTEM" in |
36 case "$ML_SYSTEM" in |
51 DISCGARB_OPTIONS="-d -c" |
52 DISCGARB_OPTIONS="-d -c" |
52 |
53 |
53 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
54 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
54 ;; |
55 ;; |
55 *) |
56 *) |
|
57 FEEDER=true |
|
58 |
56 if [ -z "$ML_DBASE" ]; then |
59 if [ -z "$ML_DBASE" ]; then |
57 ML_DBASE="$ML_HOME/ML_dbase" |
60 ML_DBASE="$ML_HOME/ML_dbase" |
58 fi |
61 fi |
59 |
62 |
60 DISCGARB="$ML_HOME/discgarb" |
63 DISCGARB="$ML_HOME/discgarb" |
67 |
70 |
68 |
71 |
69 ## prepare databases |
72 ## prepare databases |
70 |
73 |
71 if [ -z "$INFILE" ]; then |
74 if [ -z "$INFILE" ]; then |
|
75 FEEDER=true |
72 check_file "$ML_DBASE_PREFIX$ML_DBASE" |
76 check_file "$ML_DBASE_PREFIX$ML_DBASE" |
73 INFILE="$ML_DBASE" |
77 INFILE="$ML_DBASE" |
74 MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
78 MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
75 [ "$ML_SYSTEM" = polyml-4.1.3 ] && \ |
79 [ "$ML_SYSTEM" = polyml-4.1.3 ] && \ |
76 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -Smax" |
80 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" |
77 [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \ |
81 [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \ |
78 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" |
82 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" |
79 else |
83 else |
80 COPYDB=true |
84 COPYDB=true |
81 fi |
85 fi |
82 |
86 |
83 if [ -z "$OUTFILE" ]; then |
87 if [ -z "$OUTFILE" ]; then |
84 DB="$INFILE" |
88 DB="$INFILE" |
85 ML_OPTIONS="-r $ML_OPTIONS" |
89 ML_OPTIONS="-r $ML_OPTIONS" |
86 elif [ "$INFILE" -ef "$OUTFILE" ]; then |
90 elif [ "$INFILE" -ef "$OUTFILE" ]; then |
87 DB="$INFILE" |
91 DB="$INFILE" |
88 elif [ -n "$COPYDB" ]; then |
92 elif [ -n "$COPYDB" ]; then |
89 [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
93 [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
90 cp "$INFILE" "$OUTFILE" || fail_out |
94 cp "$INFILE" "$OUTFILE" || fail_out |
98 fi |
102 fi |
99 |
103 |
100 |
104 |
101 ## run it! |
105 ## run it! |
102 |
106 |
103 if [ -z "$TERMINATE" ]; then |
107 DB_INFO=$(ls -l "$DB" 2>/dev/null) |
104 FEEDER_OPTS="" |
108 |
|
109 if [ -n "$TERMINATE" ]; then |
|
110 echo "$MLTEXT" | "$POLY" $ML_OPTIONS "$DB" |
|
111 elif [ -n "$FEEDER" ]; then |
|
112 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" | \ |
|
113 { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
105 else |
114 else |
106 FEEDER_OPTS="-q" |
115 "$POLY" $ML_OPTIONS "$DB" -- "$MLTEXT" |
107 fi |
116 fi |
108 |
117 |
109 DB_INFO=$(ls -l "$DB" 2>/dev/null) |
|
110 |
|
111 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \ |
|
112 { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
|
113 RC="$?" |
118 RC="$?" |
114 |
119 |
115 |
120 |
116 NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null) |
121 NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null) |
117 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ |
122 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ |