--- a/lib/Tools/usedir Fri Dec 19 10:30:27 1997 +0100
+++ b/lib/Tools/usedir Fri Dec 19 10:31:13 1997 +0100
@@ -76,7 +76,7 @@
## main
-# prepare browser info directories
+# prepare browser info dir
if [ "$INFO" = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
@@ -96,12 +96,48 @@
fi
+# prepare log dir
+
+LOGDIR="$ISABELLE_OUTPUT/log"
+mkdir -p "$LOGDIR"
+
+
+# run isabelle
+
+SECONDS=0
+
if [ -n "$BUILD" ]; then
- exec $ISABELLE \
+ ITEM="$SESSION"
+ echo -n "Building $ITEM ... "
+ LOG="$LOGDIR/$ITEM"
+
+ $ISABELLE \
-e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
- -q -w $LOGIC $NAME
+ -q -w $LOGIC $NAME >$LOG
else
- exec $ISABELLE \
+ ITEM=$(basename $LOGIC)-"$SESSION"
+ echo -n "Running $ITEM ... "
+ LOG="$LOGDIR/$ITEM"
+
+ $ISABELLE \
-e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
- -r -q $LOGIC
+ -r -q $LOGIC > $LOG
fi
+
+RC=$?
+
+ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
+
+
+# exit status
+
+if [ $RC -eq 0 ]; then
+ echo "OK ($ELAPSED elapsed time)"
+ gzip --force "$LOG"
+else
+ echo "FAILED"
+ echo "(see also $LOG)"
+ echo; tail $LOG; echo
+fi
+
+exit $RC