# HG changeset patch
# User wenzelm
# Date 882523873 -3600
# Node ID f9e3e9f1af612bd184bbdf7337c05bcca521c3b1
# Parent  2c64ce912684479daf5541309af81eb504475ae8
log file;
elapsed time;

diff -r 2c64ce912684 -r f9e3e9f1af61 lib/Tools/usedir
--- 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