--- a/src/Pure/System/isabelle_process.scala Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala Tue Mar 15 23:59:39 2016 +0100
@@ -15,13 +15,14 @@
args: List[String] = Nil,
modes: List[String] = Nil,
secure: Boolean = false,
- receiver: Prover.Receiver = Console.println(_)): Isabelle_Process =
+ receiver: Prover.Receiver = Console.println(_),
+ store: Sessions.Store = Sessions.store()): Isabelle_Process =
{
val channel = System_Channel()
val process =
try {
ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
- channel = Some(channel))
+ channel = Some(channel), store = store)
}
catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
process.stdin.close
--- a/src/Pure/System/isabelle_system.scala Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Mar 15 23:59:39 2016 +0100
@@ -325,19 +325,7 @@
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
- /* logic images */
-
- def find_logics_dirs(): List[Path] =
- {
- val ml_ident = Path.explode("$ML_IDENTIFIER").expand
- Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
- }
-
- def find_logics(): List[String] =
- (for {
- dir <- find_logics_dirs()
- files = dir.file.listFiles() if files != null
- file <- files.toList if file.isFile } yield file.getName).sorted
+ /* default logic */
def default_logic(args: String*): String =
{
--- a/src/Pure/Thy/sessions.scala Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Mar 15 23:59:39 2016 +0100
@@ -335,16 +335,26 @@
if (system_mode) Path.explode("~~/browser_info")
else Path.explode("$ISABELLE_BROWSER_INFO")
- private val input_dirs =
+ val input_dirs =
if (system_mode) List(output_dir)
- else output_dir :: Isabelle_System.find_logics_dirs()
+ else {
+ val ml_ident = Path.explode("$ML_IDENTIFIER").expand
+ output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
+ }
+ //optional heap + log_gz
def find(name: String): Option[(Path, Path)] =
input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
(dir + Path.basic(name), dir + log_gz(name)))
- 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 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")) }
}
--- a/src/Pure/Tools/build.scala Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Pure/Tools/build.scala Tue Mar 15 23:59:39 2016 +0100
@@ -228,15 +228,17 @@
/* jobs */
- private class Job(progress: Progress,
- name: String, val info: Sessions.Info, output: Path, do_output: Boolean, verbose: Boolean,
- browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
+ private class Job(progress: Progress, name: String, val info: Sessions.Info,
+ 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))
else ""
+ output.file.delete
private val parent = info.parent.getOrElse("")
@@ -244,8 +246,6 @@
try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
catch { case ERROR(_) => /*error should be exposed in ML*/ }
- output.file.delete
-
private val env =
Isabelle_System.settings() +
("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
@@ -258,7 +258,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)
+ cwd = info.dir.file, env = env, store = store)
}
else {
val args_file = Isabelle_System.tmp_file("build")
@@ -271,7 +271,7 @@
pair(string, pair(string, pair(string,
list(pair(Options.encode, list(Path.encode)))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
- (browser_info, (info.document_files, (File.standard_path(graph_file),
+ (store.browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name,
theories)))))))))))
}))
@@ -280,8 +280,8 @@
"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)
+ ML_Process(info.options, parent, List("--eval", eval), cwd = info.dir.file,
+ env = env, cleanup = () => args_file.delete, store = store)
}
process.result(
progress_stdout = (line: String) =>
@@ -313,7 +313,7 @@
val result = future_result.join
if (result.ok && !Sessions.is_pure(name))
- Present.finish(progress, browser_info, graph_file, info, name)
+ Present.finish(progress, store.browser_info, graph_file, info, name)
graph_file.delete
timeout_request.foreach(_.cancel)
@@ -597,7 +597,6 @@
val ancestor_results = selected_tree.ancestors(name).map(results(_))
val ancestor_heaps = ancestor_results.map(_.heaps).flatten
- val output = store.output_dir + Path.basic(name)
val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
val (current, heaps) =
@@ -631,7 +630,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, output, do_output, verbose, store.browser_info,
+ new Job(progress, name, info, 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_console.scala Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala Tue Mar 15 23:59:39 2016 +0100
@@ -70,7 +70,8 @@
// process loop
val process =
ML_Process(options, heap = logic, args = List("-i"),
- modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"))
+ modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"),
+ store = Sessions.store(system_mode))
val process_output = Future.thread[Unit]("process_output") {
try {
var result = new StringBuilder(100)
--- a/src/Pure/Tools/ml_process.scala Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala Tue Mar 15 23:59:39 2016 +0100
@@ -21,7 +21,8 @@
env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
- channel: Option[System_Channel] = None): Bash.Process =
+ channel: Option[System_Channel] = None,
+ store: Sessions.Store = Sessions.store()): Bash.Process =
{
val load_heaps =
{
@@ -32,13 +33,12 @@
List(heap_path)
}
else {
- val dirs = Isabelle_System.find_logics_dirs()
- val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
- dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
+ val heap_name = Isabelle_System.default_logic(heap)
+ store.find_heap(heap_name) match {
case Some(heap_path) => List(heap_path)
case None =>
error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" +
- cat_lines(dirs.map(dir => " " + dir.implode)))
+ cat_lines(store.input_dirs.map(dir => " " + dir.implode)))
}
}
}
--- a/src/Tools/jEdit/src/isabelle_logic.scala Tue Mar 15 23:16:15 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Tue Mar 15 23:59:39 2016 +0100
@@ -76,7 +76,8 @@
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
PIDE.session.start(receiver =>
Isabelle_Process(
- PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver))
+ PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver,
+ store = Sessions.store(session_build_mode() == "system")))
}
def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))