equal
deleted
inserted
replaced
57 fi |
57 fi |
58 |
58 |
59 |
59 |
60 ## run it! |
60 ## run it! |
61 |
61 |
62 START_POLY="$POLY $ML_OPTIONS $DB" |
62 if [ -z "$TERMINATE" ]; then |
|
63 FEEDER_OPTS="-s" |
|
64 else |
|
65 FEEDER_OPTS="-q" |
|
66 fi |
|
67 |
63 DB_INFO=$(ls -l "$DB") |
68 DB_INFO=$(ls -l "$DB") |
64 |
69 |
65 if [ -n "$TERMINATE" ]; then |
70 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \ |
66 echo "$MLTEXT" | $START_POLY |
71 { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; } |
67 RC=$? |
72 RC=$? |
68 elif [ -z "$MLTEXT" ]; then |
|
69 sh -c "$ISABELLE_HOME/lib/Tools/symbolinput | $START_POLY" |
|
70 RC=$? |
|
71 else |
|
72 sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; } | $START_POLY" |
|
73 RC=$? |
|
74 fi |
|
75 |
73 |
76 NEW_DB_INFO=$(ls -l "$DB") |
74 NEW_DB_INFO=$(ls -l "$DB") |
77 [ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE" |
75 [ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE" |
78 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
76 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
79 |
77 |
80 exit $RC |
78 exit $RC |