lib/Tools/build

 
 
 ## diagnostics
 
 PRG="$(basename "$0")"
+
+function show_settings()
+{
+  local PREFIX="$1"
+  echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
+  echo
+  echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
+  echo "${PREFIX}ML_HOME=\"$ML_HOME\""
+  echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
+  echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
+}
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"

   echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo "    -t           inner session timing"
   echo "    -v           verbose"
   echo
   echo "  Build and manage Isabelle sessions, depending on implicit"
-  echo "  ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
-  echo
-  echo "  ML_PLATFORM=\"$ML_PLATFORM\""
-  echo "  ML_HOME=\"$ML_HOME\""
-  echo "  ML_SYSTEM=\"$ML_SYSTEM\""
-  echo "  ML_OPTIONS=\"$ML_OPTIONS\""
+  show_settings "  "
   echo
   exit 1
 }
 
 function fail()

 
 ## main
 
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
-exec "$ISABELLE_TOOL" java isabelle.Build \
+if [ "$NO_BUILD" = false ]; then
+  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+
+  if [ "$VERBOSE" = true ]; then
+    show_settings ""
+    echo
+  fi
+  . "$ISABELLE_HOME/lib/scripts/timestart.bash"
+fi
+
+"$ISABELLE_TOOL" java isabelle.Build \
   "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \
   "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+RC="$?"
+
+if [ "$NO_BUILD" = false ]; then
+  echo -n "Finished at "; date
+
+  . "$ISABELLE_HOME/lib/scripts/timestop.bash"
+  echo "$TIMES_REPORT"
+fi
+
+exit "$RC"