# HG changeset patch
# User wenzelm
# Date 876154815 -7200
# Node ID b1bfd394b60aa5c45e297818e1f7e3be0311fb30
# Parent  989ef5e9d543c4927e06fbcc288189016ddf0d5a
RAW target;

diff -r 989ef5e9d543 -r b1bfd394b60a src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Oct 06 09:26:00 1997 +0200
+++ b/src/Pure/IsaMakefile	Mon Oct 06 18:20:15 1997 +0200
@@ -21,9 +21,12 @@
 	search.ML section_utils.ML sequence.ML sign.ML sorts.ML symtab.ML tactic.ML \
 	tctical.ML term.ML theory.ML thm.ML type.ML type_infer.ML unify.ML
 
-$(OUT)/Pure: $(FILES)
+Pure: $(FILES)
 	@./mk
 
-test: $(OUT)/Pure
+RAW: $(FILES)
+	@./mk -r
+
+test: Pure
 
 .PRECIOUS: $(OUT)/Pure
diff -r 989ef5e9d543 -r b1bfd394b60a src/Pure/mk
--- a/src/Pure/mk	Mon Oct 06 09:26:00 1997 +0200
+++ b/src/Pure/mk	Mon Oct 06 18:20:15 1997 +0200
@@ -9,6 +9,18 @@
 
 ## diagnostics
 
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS]"
+  echo
+  echo "  Make Pure Isabelle."
+  echo
+  echo "    -r           just prepare RAW image"
+  echo
+  exit 1
+}
+
 function fail()
 {
   echo "$1" >&2
@@ -16,6 +28,32 @@
 }
 
 
+## process command line
+
+# options
+
+RAW=""
+
+while getopts "r" OPT
+do
+  case "$OPT" in
+    r)
+      RAW=true
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ $# -ne 0 ] && usage
+
+
 ## main
 
 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
@@ -27,7 +65,14 @@
 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
 
-$ISABELLE \
-  -e "val ml_system = \"$ML_SYSTEM\";" \
-  -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
-  -q -w RAW_ML_SYSTEM Pure
+if [ -z "$RAW" ]; then
+  $ISABELLE \
+    -e "val ml_system = \"$ML_SYSTEM\";" \
+    -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
+    -q -w RAW_ML_SYSTEM Pure
+else
+  $ISABELLE \
+    -e "val ml_system = \"$ML_SYSTEM\";" \
+    -e "use\"$COMPAT\";" \
+    -q -w RAW_ML_SYSTEM RAW
+fi