diff -r 89d58ed34299 -r 18937ee21db7 src/Pure/mk
--- 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"