src/Pure/Tools/build.scala

     session_content(options, false, Nil, session).syntax
 
 
   /* 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])
   {
     val output = store.output_dir + Path.basic(name)
     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
 
     private val parent = info.parent.getOrElse("")
 

           if (Sessions.is_pure(name)) {
             val eval =
               "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")
             File.write(args_file, YXML.string_of_body(
                 {

               "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, store = store)
+              env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
           }
         process.result(
           progress_stdout = (line: String) =>
             Library.try_unprefix("\floading_theory = ", line) match {
               case Some(theory) => progress.theory(name, theory)

                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)))))
                 }
                 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)
                 }
                 else {
                   progress.echo(name + " CANCELLED")