--- a/src/Pure/Tools/build.scala Mon Feb 29 20:43:16 2016 +0100
+++ b/src/Pure/Tools/build.scala Mon Feb 29 21:32:53 2016 +0100
@@ -572,36 +572,57 @@
File.standard_path(args_file))
private val script =
- if (is_pure(name)) {
- if (do_output) "./build " + name + " \"$OUTPUT\""
- else "./build " + name
- }
- else {
- """
- . "$ISABELLE_HOME/lib/scripts/timestart.bash"
- """ +
- (if (do_output)
- """
+ """
+ . "$ISABELLE_HOME/lib/scripts/timestart.bash"
+ """ +
+ (if (is_pure(name)) {
+ val ml_system = Isabelle_System.getenv("ML_SYSTEM")
+ val ml_system_base = Library.space_explode('-', ml_system).headOption getOrElse ml_system
+ val ml_root =
+ List(ml_system, ml_system_base).map(a => "RAW/ROOT_" + a + ".ML").
+ find(b => Path.explode("~~/src/Pure/" + b).file.isFile) getOrElse
+ error("Missing compatibility file for ML system " + quote(ml_system))
+
+ if (name == "RAW") {
+ """
+ rm -f "$OUTPUT"
+ "$ISABELLE_PROCESS" \
+ -e 'use """ + quote(ml_root) + """ 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"
+ """
+ }
+ else {
+ """
rm -f "$OUTPUT"
- "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT"
- """
- else
- """
- rm -f "$OUTPUT"
- "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT"
- """) +
+ "$ISABELLE_PROCESS" \
+ -e '(use """ + quote(ml_root) + """; 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"
+ """
+ }
+ }
+ else if (do_output)
"""
- RC="$?"
+ rm -f "$OUTPUT"
+ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT"
+ """
+ else
+ """
+ rm -f "$OUTPUT"
+ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT"
+ """) +
+ """
+ RC="$?"
- . "$ISABELLE_HOME/lib/scripts/timestop.bash"
+ . "$ISABELLE_HOME/lib/scripts/timestop.bash"
- if [ "$RC" -eq 0 ]; then
- echo "Finished $TARGET ($TIMES_REPORT)" >&2
- fi
+ if [ "$RC" -eq 0 ]; then
+ echo "Finished $TARGET ($TIMES_REPORT)" >&2
+ fi
- exit "$RC"
- """
- }
+ exit "$RC"
+ """
private val result =
Future.thread("build") {
@@ -923,7 +944,7 @@
case Some(parent) => results(parent)
}
val output = output_dir + Path.basic(name)
- val do_output = build_heap || queue.is_inner(name)
+ val do_output = build_heap || is_pure(name) || queue.is_inner(name)
val (current, heap) =
{
--- 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"