--- a/src/Pure/mk Thu Jan 04 17:49:41 2007 +0100
+++ b/src/Pure/mk Thu Jan 04 17:49:42 2007 +0100
@@ -17,8 +17,8 @@
echo
echo " Make Pure Isabelle."
echo
- echo " -C tell ML system to copy output image"
- echo " -r prepare RAW image only"
+ echo " -R DIR/FILE run RAW session"
+ echo " -r build RAW image"
echo
exit 1
}
@@ -34,14 +34,14 @@
# options
-COPY=""
+RAW_SESSION=""
RAW=""
-while getopts "Cr" OPT
+while getopts "R:r" OPT
do
case "$OPT" in
- C)
- COPY="-C"
+ R)
+ RAW_SESSION="$OPTARG"
;;
r)
RAW=true
@@ -83,28 +83,37 @@
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-if [ -z "$RAW" ]; then
+if [ -n "$RAW" ]; then
+ ITEM="RAW"
+ echo "Building $ITEM ..."
+ LOG="$LOGDIR/$ITEM"
+
+ "$ISABELLE" \
+ -e "val ml_system = \"$ML_SYSTEM\";" \
+ -e "val ml_platform = \"$ML_PLATFORM\";" \
+ -e "use\"$COMPAT\" handle _ => exit 1;" \
+ -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
+ RC="$?"
+elif [ -n "$RAW_SESSION" ]; then
+ ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
+ echo "Building $ITEM ..."
+ LOG="$LOGDIR/$ITEM"
+
+ "$ISABELLE" \
+ -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
+ -q RAW > "$LOG" 2>&1
+ RC="$?"
+else
ITEM="Pure"
echo "Building $ITEM ..."
LOG="$LOGDIR/$ITEM"
- "$ISABELLE" $COPY \
+ "$ISABELLE" \
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "val ml_platform = \"$ML_PLATFORM\";" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
RC="$?"
-else
- ITEM="RAW"
- echo "Building $ITEM ..."
- LOG="$LOGDIR/$ITEM"
-
- "$ISABELLE" $COPY \
- -e "val ml_system = \"$ML_SYSTEM\";" \
- -e "val ml_platform = \"$ML_PLATFORM\";" \
- -e "use\"$COMPAT\" handle _ => exit 1;" \
- -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
- RC="$?"
fi
. "$ISABELLE_HOME/lib/scripts/timestop.bash"