# HG changeset patch
# User wenzelm
# Date 1456777973 -3600
# Node ID bc6e771e98a6d3819a84c6ef0644951111a06e41
# Parent  d396da07055db77bd5c19c207fff0ec188b619d6
simplified -- always produce heap for RAW, Pure;

diff -r d396da07055d -r bc6e771e98a6 src/Pure/Tools/build.scala
--- 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) =
                 {
diff -r d396da07055d -r bc6e771e98a6 src/Pure/build
--- 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"