--- 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)))
}
}
--- 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)
}
--- 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),