--- a/src/Pure/build Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/build Fri Jul 20 21:04:03 2012 +0200
@@ -12,7 +12,10 @@
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
@@ -30,6 +33,27 @@
## 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\""
@@ -54,29 +78,37 @@
. "$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"