src/Pure/Tools/build.scala

--- a/src/Pure/Tools/build.scala	Wed Mar 09 16:53:14 2016 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 09 19:30:09 2016 +0100
@@ -550,6 +550,7 @@
     catch { case ERROR(_) => /*error should be exposed in ML*/ }
 
     private val args_file = Isabelle_System.tmp_file("args")
+    private val args_standard_path = File.standard_path(args_file)
     File.write(args_file, YXML.string_of_body(
       if (is_pure(name)) Options.encode(info.options)
       else
@@ -566,48 +567,28 @@
             theories))))))))))))
         }))
 
-    private val env =
-    {
-      val env0 =
-        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
-          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
-            File.standard_path(args_file))
-      if (is_pure(name))
-        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
-      else env0
-    }
+    output.file.delete
+
+    private val env = Map("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
 
-    private val script =
-      """
-      . "$ISABELLE_HOME/lib/scripts/timestart.bash"
-      """ +
-      (if (is_pure(name))
-        """
-          rm -f "$OUTPUT"
-          "$ISABELLE_PROCESS" -f "ROOT.ML" \
-            -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
-        """
-      else
-        """
-        rm -f "$OUTPUT"
-        "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT"
-        """) +
-      """
-      RC="$?"
-
-      . "$ISABELLE_HOME/lib/scripts/timestop.bash"
-
-      if [ "$RC" -eq 0 ]; then
-        echo "Finished $TARGET ($TIMES_REPORT)" >&2
-      fi
-
-      exit "$RC"
-      """
-
-    private val future_result =
+    private val future_result: Future[Process_Result] =
       Future.thread("build") {
-        Isabelle_System.bash(script, info.dir.file, env,
+        val process =
+          if (is_pure(name)) {
+            val eval =
+              "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
+              " Session.shutdown (); ML_Heap.share_common_data ();" +
+              " ML_Heap.save_state " + ML_Syntax.print_string_raw(output_standard_path) + "));"
+            val env1 = env + ("ISABELLE_PROCESS_OPTIONS" -> args_standard_path)
+            ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
+              cwd = info.dir.file, env = env1)
+          }
+          else {
+            ML_Process(info.options, parent,
+              List("--eval", "Build.build " + ML_Syntax.print_string_raw(args_standard_path)),
+              cwd = info.dir.file, env = env)
+          }
+        process.result(
           progress_stdout = (line: String) =>
             Library.try_unprefix("\floading_theory = ", line) match {
               case Some(theory) => progress.theory(name, theory)
@@ -876,7 +857,9 @@
             //{{{ finish job
 
             val process_result = job.join
-            progress.echo(process_result.err)
+            process_result.err_lines.foreach(progress.echo(_))
+            if (process_result.ok)
+              progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
 
             val process_result_tail =
             {