# HG changeset patch
# User wenzelm
# Date 1344420814 -7200
# Node ID 519b6e53179b33446f0d26e9b81ee5114694aab9
# Parent  093eb27374bb475dc8ca7d7be694500c5cfd4151
obsolete;

diff -r 093eb27374bb -r 519b6e53179b src/Pure/mk
--- a/src/Pure/mk	Wed Aug 08 12:10:22 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# mk - build Isabelle/Pure.
-#
-# Requires proper Isabelle settings environment.
-
-
-## diagnostics
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG [OPTIONS]"
-  echo
-  echo "  Make Pure Isabelle."
-  echo
-  echo "    -R DIR/FILE  run RAW session"
-  echo "    -r           build RAW image"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-RAW_SESSION=""
-RAW=""
-
-while getopts "R:r" OPT
-do
-  case "$OPT" in
-    R)
-      RAW_SESSION="$OPTARG"
-      ;;
-    r)
-      RAW=true
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-# get compatibility file
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
-
-COMPAT=""
-[ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"
-[ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
-[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
-
-
-# prepare log dir
-
-LOGDIR="$ISABELLE_OUTPUT/log"
-mkdir -p "$LOGDIR"
-
-
-# run isabelle
-
-. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-
-if [ -n "$RAW" ]; then
-  ITEM="RAW"
-  echo "Building $ITEM ..."
-  LOG="$LOGDIR/$ITEM"
-
-  "$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 > "$LOG" 2>&1
-  RC="$?"
-elif [ -n "$RAW_SESSION" ]; then
-  ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
-  echo "Running $ITEM ..."
-  LOG="$LOGDIR/$ITEM"
-
-  "$ISABELLE_PROCESS" \
-    -e "use\"$RAW_SESSION\" handle _ => exit 1;" \
-    -q RAW > "$LOG" 2>&1
-  RC="$?"
-else
-  ITEM="Pure"
-  echo "Building $ITEM ..."
-  LOG="$LOGDIR/$ITEM"
-
-  "$ISABELLE_PROCESS" \
-    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-    -e "ml_prompts \"ML> \" \"ML# \";" \
-    -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
-  RC="$?"
-fi
-
-. "$ISABELLE_HOME/lib/scripts/timestop.bash"
-
-
-# exit status
-
-if [ "$RC" -eq 0 ]; then
-  echo "Finished $ITEM ($TIMES_REPORT)"
-  gzip --force "$LOG"
-else
-  echo "$ITEM FAILED"
-  echo "(see also $LOG)"
-  echo; tail "$LOG"; echo
-fi
-
-exit "$RC"