# HG changeset patch # User wenzelm # Date 1458082779 -3600 # Node ID e57416b649d5f0612a013bb976608184ec1650e1 # Parent cd991ba01ffd1bde67d6973832ab9ae0d2000a0e find heaps uniformly via Sessions.Store; tuned; diff -r cd991ba01ffd -r e57416b649d5 src/Pure/System/isabelle_process.scala --- 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 diff -r cd991ba01ffd -r e57416b649d5 src/Pure/System/isabelle_system.scala --- 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 = { diff -r cd991ba01ffd -r e57416b649d5 src/Pure/Thy/sessions.scala --- 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")) } } diff -r cd991ba01ffd -r e57416b649d5 src/Pure/Tools/build.scala --- 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) } diff -r cd991ba01ffd -r e57416b649d5 src/Pure/Tools/ml_console.scala --- 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) diff -r cd991ba01ffd -r e57416b649d5 src/Pure/Tools/ml_process.scala --- 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))) } } } diff -r cd991ba01ffd -r e57416b649d5 src/Tools/jEdit/src/isabelle_logic.scala --- 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"))