# HG changeset patch
# User wenzelm
# Date 882522926 -3600
# Node ID 8ed9e689a15e00da6cabd1b14382ec9a1c06e4eb
# Parent  42cdcacb60e2237a852d29cd29c75b453e682e64
log file;
elapsed time;

diff -r 42cdcacb60e2 -r 8ed9e689a15e src/Pure/mk
--- a/src/Pure/mk	Fri Dec 19 10:14:55 1997 +0100
+++ b/src/Pure/mk	Fri Dec 19 10:15:26 1997 +0100
@@ -56,6 +56,8 @@
 
 ## main
 
+# get compatibility file
+
 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
 [ -z "$ML_SYSTEM" ] && \
   fail "Missing ML system settings! Probably not run via 'isatool make'?."
@@ -65,14 +67,51 @@
 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
 
+
+# prepare log dir
+
+LOGDIR="$ISABELLE_OUTPUT/log"
+mkdir -p "$LOGDIR"
+
+
+# run isabelle
+
+SECONDS=0
+
 if [ -z "$RAW" ]; then
+  ITEM="Pure"
+  echo -n "Building $ITEM ... "
+  LOG="$LOGDIR/$ITEM"
+
   $ISABELLE \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
-    -q -w RAW_ML_SYSTEM Pure
+    -q -w RAW_ML_SYSTEM Pure > $LOG
 else
+  ITEM="RAW"
+  echo -n "Building $ITEM ... "
+  LOG="$LOGDIR/$ITEM"
+
   $ISABELLE \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "use\"$COMPAT\";" \
-    -q -w RAW_ML_SYSTEM RAW
+    -q -w RAW_ML_SYSTEM RAW > $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