# HG changeset patch
# User wenzelm
# Date 1458137302 -3600
# Node ID 0189fe0f64529da0e5f80a381cac5f08a07ccf2e
# Parent  e676ae9f1bf63ae5dfe0184b240e1b03fb23b850
support for Poly/ML heap hierarchy, which saves a lot of disk space;

diff -r e676ae9f1bf6 -r 0189fe0f6452 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Mar 16 14:24:51 2016 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 16 15:08:22 2016 +0100
@@ -318,7 +318,8 @@
   }
 
 
-  /* persistent store */
+
+  /** persistent store **/
 
   def log(name: String): Path = Path.basic("log") + Path.basic(name)
   def log_gz(name: String): Path = log(name).ext("gz")
@@ -327,15 +328,22 @@
 
   class Store private [Sessions](system_mode: Boolean)
   {
-    val output_dir: Path =
-      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
-      else Path.explode("$ISABELLE_OUTPUT")
+    /* output */
 
     val browser_info: Path =
       if (system_mode) Path.explode("~~/browser_info")
       else Path.explode("$ISABELLE_BROWSER_INFO")
 
-    val input_dirs =
+    val output_dir: Path =
+      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
+      else Path.explode("$ISABELLE_OUTPUT")
+
+    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
+
+
+    /* input */
+
+    private val input_dirs =
       if (system_mode) List(output_dir)
       else {
         val ml_ident = Path.explode("$ML_IDENTIFIER").expand
@@ -346,15 +354,18 @@
       input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
         (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
 
-    def find_heap(name: String): Option[Path] =
-      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
-
     def find_log(name: String): Option[Path] =
       input_dirs.map(_ + log(name)).find(_.is_file)
 
     def find_log_gz(name: String): Option[Path] =
       input_dirs.map(_ + log_gz(name)).find(_.is_file)
 
-    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
+    def find_heap(name: String): Option[Path] =
+      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
+
+    def heap(name: String): Path =
+      find_heap(name) getOrElse
+        error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
+          cat_lines(input_dirs.map(dir => "  " + dir.implode)))
   }
 }
diff -r e676ae9f1bf6 -r 0189fe0f6452 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 16 14:24:51 2016 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 16 15:08:22 2016 +0100
@@ -228,7 +228,7 @@
 
   /* jobs */
 
-  private class Job(progress: Progress, name: String, val info: Sessions.Info,
+  private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
     store: Sessions.Store, do_output: Boolean, verbose: Boolean,
     session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
   {
@@ -236,7 +236,8 @@
     def output_path: Option[Path] = if (do_output) Some(output) else None
     def output_save_state: String =
       if (do_output)
-        "PolyML.SaveState.saveState " + ML_Syntax.print_string_raw(File.platform_path(output))
+        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string_raw(File.platform_path(output)) +
+          ", List.length (PolyML.SaveState.showHierarchy ()))"
       else ""
     output.file.delete
 
@@ -258,7 +259,7 @@
               "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
               " 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, store = store)
+              cwd = info.dir.file, env = env, tree = Some(tree), store = store)
           }
           else {
             val args_file = Isabelle_System.tmp_file("build")
@@ -281,7 +282,7 @@
               (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, store = store)
+              env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
           }
         process.result(
           progress_stdout = (line: String) =>
@@ -622,7 +623,7 @@
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
                   val job =
-                    new Job(progress, name, info, store, do_output, verbose,
+                    new Job(progress, name, info, selected_tree, store, do_output, verbose,
                       deps(name).session_graph, queue.command_timings(name))
                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
                 }
diff -r e676ae9f1bf6 -r 0189fe0f6452 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Wed Mar 16 14:24:51 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 15:08:22 2016 +0100
@@ -15,6 +15,7 @@
   def apply(options: Options,
     logic: String = "",
     args: List[String] = Nil,
+    dirs: List[Path] = Nil,
     modes: List[String] = Nil,
     secure: Boolean = false,
     cwd: JFile = null,
@@ -22,28 +23,19 @@
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None,
+    tree: Option[Sessions.Tree] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
-    val heaps =
-      Isabelle_System.default_logic(logic) match {
-        case "RAW_ML_SYSTEM" => Nil
-        case name =>
-          store.find_heap(name) match {
-            case Some(path) => List(path)
-            case None =>
-              error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
-                cat_lines(store.input_dirs.map(dir => "  " + dir.implode)))
-          }
+    val logic_name = Isabelle_System.default_logic(logic)
+    val heaps: List[String] =
+      if (logic_name == "RAW_ML_SYSTEM") Nil
+      else {
+        val session_tree = tree.getOrElse(Sessions.load(options, dirs))
+        (session_tree.ancestors(logic_name) ::: List(logic_name)).
+          map(a => File.platform_path(store.heap(a)))
       }
 
-    val eval_heaps =
-      heaps.map(heap =>
-        "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(heap)) +
-        "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
-        ML_Syntax.print_string_raw(": " + heap.toString + "\n") +
-        "); OS.Process.exit OS.Process.failure)")
-
-    val eval_initial =
+    val eval_init =
       if (heaps.isEmpty) {
         List(
           if (Platform.is_windows)
@@ -55,7 +47,13 @@
           "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
           "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
       }
-      else Nil
+      else
+        List(
+          "(PolyML.SaveState.loadHierarchy " +
+            ML_Syntax.print_list(ML_Syntax.print_string_raw)(heaps) +
+          "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
+          ML_Syntax.print_string_raw(": " + logic_name + "\n") +
+          "); OS.Process.exit OS.Process.failure)")
 
     val eval_modes =
       if (modes.isEmpty) Nil
@@ -88,7 +86,7 @@
     // bash
     val bash_args =
       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
-      (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
+      (eval_init ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
     Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),