--- a/src/Pure/build Mon Feb 29 20:43:16 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# build - build Isabelle/ML
-#
-# Requires proper Isabelle settings environment.
-
-
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG TARGET [OUTPUT]"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
-
-
-## process command line
-
-# args
-
-if [ "$#" -eq 1 ]; then
- TARGET="$1"; shift
- OUTPUT=""; shift
-elif [ "$#" -eq 2 ]; then
- TARGET="$1"; shift
- OUTPUT="$1"; shift
-else
- usage
-fi
-
-
-## main
-
-# get compatibility file
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
-
-COMPAT=""
-[ -f "RAW/ROOT_${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM_BASE}.ML"
-[ -f "RAW/ROOT_${ML_SYSTEM}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM}.ML"
-[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
-
-
-# run isabelle
-
-. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-
-if [ "$TARGET" = RAW ]; then
- if [ -z "$OUTPUT" ]; then
- "$ISABELLE_PROCESS" \
- -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
- -q RAW_ML_SYSTEM
- else
- rm -f "$OUTPUT"
- "$ISABELLE_PROCESS" \
- -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
- -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
- -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
- fi
-else
- if [ -z "$OUTPUT" ]; then
- "$ISABELLE_PROCESS" \
- -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
- -q RAW_ML_SYSTEM
- else
- rm -f "$OUTPUT"
- "$ISABELLE_PROCESS" \
- -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
- -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
- -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
- fi
-fi
-
-RC="$?"
-
-. "$ISABELLE_HOME/lib/scripts/timestop.bash"
-
-if [ "$RC" -eq 0 ]; then
- echo "Finished $TARGET ($TIMES_REPORT)" >&2
-fi
-
-exit "$RC"