ML save_state under control of Isabelle/Scala;

--- a/src/Pure/ML/ml_heap.ML	Tue Mar 15 14:30:18 2016 +0100
+++ b/src/Pure/ML/ml_heap.ML	Tue Mar 15 16:23:27 2016 +0100
@@ -7,11 +7,9 @@
 signature ML_HEAP =
 sig
   val share_common_data: unit -> unit
-  val save_state: string -> unit
 end;
 
 structure ML_Heap: ML_HEAP =
 struct
   fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
 end;

--- a/src/Pure/Tools/build.ML	Tue Mar 15 14:30:18 2016 +0100
+++ b/src/Pure/Tools/build.ML	Tue Mar 15 16:23:27 2016 +0100
@@ -120,54 +120,52 @@
         " (undefined " ^ commas conds ^ ")\n")
   end;
 
-fun build args_file = Command_Line.tool0 (fn () =>
-    let
-      val _ = SHA1_Samples.test ();
+fun build args_file =
+  let
+    val _ = SHA1_Samples.test ();
 
-      val (symbol_codes, (command_timings, (output, (verbose, (browser_info,
-            (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
-        File.read (Path.explode args_file) |> YXML.parse_body |>
-          let open XML.Decode in
-            pair (list (pair string int)) (pair (list properties) (pair string
-              (pair bool (pair string (pair (list (pair string string)) (pair string
-                (pair string (pair string (pair string
-                ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
-          end;
-      val do_output = output <> "";
+    val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
+          (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
+      File.read (Path.explode args_file) |> YXML.parse_body |>
+        let open XML.Decode in
+          pair (list (pair string int)) (pair (list properties) (pair bool
+            (pair bool (pair string (pair (list (pair string string)) (pair string
+              (pair string (pair string (pair string
+              ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
+        end;
 
-      val symbols = HTML.make_symbols symbol_codes;
-      val _ = Isabelle_Process.init_build_options ();
+    val symbols = HTML.make_symbols symbol_codes;
+    val _ = Isabelle_Process.init_build_options ();
 
-      val _ = writeln ("\fSession.name = " ^ name);
-      val _ =
-        Session.init
-          symbols
-          do_output
-          (Options.default_bool "browser_info")
-          (Path.explode browser_info)
-          (Options.default_string "document")
-          (Options.default_string "document_output")
-          (Present.document_variants (Options.default_string "document_variants"))
-          (map (apply2 Path.explode) document_files)
-          (Path.explode graph_file)
-          parent_name (chapter, name)
-          verbose;
+    val _ = writeln ("\fSession.name = " ^ name);
+    val _ =
+      Session.init
+        symbols
+        do_output
+        (Options.default_bool "browser_info")
+        (Path.explode browser_info)
+        (Options.default_string "document")
+        (Options.default_string "document_output")
+        (Present.document_variants (Options.default_string "document_variants"))
+        (map (apply2 Path.explode) document_files)
+        (Path.explode graph_file)
+        parent_name (chapter, name)
+        verbose;
 
-      val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
+    val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
 
-      val res1 =
-        theories |>
-          (List.app (build_theories symbols last_timing Path.current)
-            |> session_timing name verbose
-            |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
-            |> Multithreading.max_threads_setmp (Options.default_int "threads")
-            |> Exn.capture);
-      val res2 = Exn.capture Session.finish ();
-      val _ = Par_Exn.release_all [res1, res2];
+    val res1 =
+      theories |>
+        (List.app (build_theories symbols last_timing Path.current)
+          |> session_timing name verbose
+          |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
+          |> Multithreading.max_threads_setmp (Options.default_int "threads")
+          |> Exn.capture);
+    val res2 = Exn.capture Session.finish ();
+    val _ = Par_Exn.release_all [res1, res2];
 
-      val _ = Options.reset_default ();
-      val _ = if do_output then (ML_Heap.share_common_data (); ML_Heap.save_state output) else ();
-    in () end);
+    val _ = Options.reset_default ();
+  in () end;
 
 
 (* PIDE protocol *)

--- a/src/Pure/Tools/build.scala	Tue Mar 15 14:30:18 2016 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 15 16:23:27 2016 +0100
@@ -544,7 +544,10 @@
     browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
   {
     def output_path: Option[Path] = if (do_output) Some(output) else None
-    def output_standard_path: String = if (do_output) File.standard_path(output) else ""
+    def output_save_state: String =
+      if (do_output)
+        "PolyML.SaveState.saveState " + ML_Syntax.print_string_raw(File.platform_path(output))
+      else ""
 
     private val parent = info.parent.getOrElse("")
 
@@ -564,8 +567,7 @@
           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) + "));"
+              " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
             ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
               cwd = info.dir.file, env = env)
           }
@@ -575,18 +577,21 @@
                 {
                   val theories = info.theories.map(x => (x._2, x._3))
                   import XML.Encode._
-                  pair(list(pair(string, int)), pair(list(properties), pair(string, pair(bool,
+                  pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                     pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                     pair(string, pair(string, pair(string,
                     list(pair(Options.encode, list(Path.encode)))))))))))))(
-                  (Symbol.codes, (command_timings, (output_standard_path, (verbose,
+                  (Symbol.codes, (command_timings, (do_output, (verbose,
                     (browser_info, (info.document_files, (File.standard_path(graph_file),
                     (parent, (info.chapter, (name,
                     theories)))))))))))
                 }))
-            ML_Process(info.options, parent,
-              List("--eval",
-                "Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file))),
+            val eval =
+              "Command_Line.tool0 (fn () => (" +
+              "Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file)) +
+              (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
+               else "") + "));"
+            ML_Process(info.options, parent, List("--eval", eval),
               cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
           }
         process.result(