# HG changeset patch
# User wenzelm
# Date 1133458906 -3600
# Node ID 3414557c2dda81e83bc725e9f648faf32b2f6749
# Parent  ce523820ff75e1311976ba53421dc0dca3220eb4
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;

diff -r ce523820ff75 -r 3414557c2dda build
--- a/build	Thu Dec 01 18:41:44 2005 +0100
+++ b/build	Thu Dec 01 18:41:46 2005 +0100
@@ -169,8 +169,8 @@
 
 # build it
 
-SECONDS=0
 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 for L in $MAKE_LOGICS
 do
@@ -179,5 +179,5 @@
 
 echo -n "Finished at "; date
 
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
-echo "$ELAPSED total elapsed time"
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
+echo "$TIMES_REPORT"
diff -r ce523820ff75 -r 3414557c2dda lib/Tools/makeall
--- a/lib/Tools/makeall	Thu Dec 01 18:41:44 2005 +0100
+++ b/lib/Tools/makeall	Thu Dec 01 18:41:46 2005 +0100
@@ -37,6 +37,7 @@
 FAIL=""
 
 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 for L in $ALL_LOGICS
 do
@@ -45,7 +46,7 @@
 
 echo -n "Finished at "; date
 
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
-echo "$ELAPSED total elapsed time"
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
+echo "$TIMES_REPORT"
 
 [ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"
diff -r ce523820ff75 -r 3414557c2dda lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Dec 01 18:41:44 2005 +0100
+++ b/lib/Tools/usedir	Thu Dec 01 18:41:46 2005 +0100
@@ -198,7 +198,7 @@
 fi
 
 
-SECONDS=0
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 if [ -n "$BUILD" ]; then
   ITEM="$SESSION"
@@ -224,13 +224,13 @@
   cd ..
 fi
 
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
 
 
 # exit status
 
 if [ "$RC" -eq 0 ]; then
-  echo "Finished $ITEM ($ELAPSED elapsed time)" >&2
+  echo "Finished $ITEM ($TIMES_REPORT)" >&2
   gzip --force "$LOG"
 else
   { echo "$ITEM FAILED";
diff -r ce523820ff75 -r 3414557c2dda src/Pure/mk
--- a/src/Pure/mk	Thu Dec 01 18:41:44 2005 +0100
+++ b/src/Pure/mk	Thu Dec 01 18:41:46 2005 +0100
@@ -81,7 +81,7 @@
 
 # run isabelle
 
-SECONDS=0
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 if [ -z "$RAW" ]; then
   ITEM="Pure"
@@ -107,13 +107,13 @@
   RC="$?"
 fi
 
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
 
 
 # exit status
 
 if [ "$RC" -eq 0 ]; then
-  echo "Finished $ITEM ($ELAPSED elapsed time)"
+  echo "Finished $ITEM ($TIMES_REPORT)"
   gzip --force "$LOG"
 else
   echo "$ITEM FAILED"