src/Pure/build

 ## diagnostics
 
 function usage()
 {
   echo
-  echo "Usage: $PRG TARGET"
+  echo "Usage: $PRG [OPTIONS] TARGET"
+  echo
+  echo "  Options are:"
+  echo "    -b           build target images"
   echo
   echo "  Build Isabelle/ML TARGET: RAW or Pure"
   echo
   exit 1
 }

 
 [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
 
 
 ## process command line
+
+# options
+
+BUILD_IMAGES=false
+
+while getopts "b" OPT
+do
+  case "$OPT" in
+    b)
+      BUILD_IMAGES="true"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
 
 TARGET="Pure"
 [ "$#" -ge 1 ] && { TARGET="$1"; shift; }
 [ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
 

 
 # run isabelle
 
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
-echo "Building $TARGET ..." >&2
+if [ "$TARGET" = RAW ]; then
+  if [ "$BUILD_IMAGES" = false ]; then
+    "$ISABELLE_PROCESS" \
+      -e "use\"$COMPAT\" handle _ => exit 1;" \
+      -q RAW_ML_SYSTEM
+  else
+    "$ISABELLE_PROCESS" \
+      -e "use\"$COMPAT\" handle _ => exit 1;" \
+      -e "structure Isar = struct fun main () = () end;" \
+      -e "ml_prompts \"ML> \" \"ML# \";" \
+      -q -w RAW_ML_SYSTEM RAW
+  fi
+else
+  if [ "$BUILD_IMAGES" = false ]; then
+    "$ISABELLE_PROCESS" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+      -q RAW_ML_SYSTEM
+  else
+    "$ISABELLE_PROCESS" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+      -e "ml_prompts \"ML> \" \"ML# \";" \
+      -f -q -w RAW_ML_SYSTEM Pure
+  fi
+fi
 
-if [ "$TARGET" = RAW ]; then
-  "$ISABELLE_PROCESS" \
-    -e "use\"$COMPAT\" handle _ => exit 1;" \
-    -e "structure Isar = struct fun main () = () end;" \
-    -e "ml_prompts \"ML> \" \"ML# \";" \
-    -q -w RAW_ML_SYSTEM RAW
-  RC="$?"
-else
-  "$ISABELLE_PROCESS" \
-    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-    -e "ml_prompts \"ML> \" \"ML# \";" \
-    -f -q -w RAW_ML_SYSTEM Pure
-  RC="$?"
-fi
+RC="$?"
 
 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
 
 if [ "$RC" -eq 0 ]; then
   echo "Finished $TARGET ($TIMES_REPORT)" >&2
-else
-  echo "$TARGET FAILED" >&2
 fi
 
 exit "$RC"