# HG changeset patch # User wenzelm # Date 1458080175 -3600 # Node ID cd991ba01ffd1bde67d6973832ab9ae0d2000a0e # Parent c39614ddb80be38966d240f1d49e7fa1bd509017 clarified modules; diff -r c39614ddb80b -r cd991ba01ffd src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Mar 15 22:01:26 2016 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Mar 15 23:16:15 2016 +0100 @@ -316,4 +316,36 @@ info <- find_dir(select, dir) } yield info) } + + + /* persistent store */ + + def log(name: String): Path = Path.basic("log") + Path.basic(name) + def log_gz(name: String): Path = log(name).ext("gz") + + def store(system_mode: Boolean = false): Store = new Store(system_mode) + + class Store private [Sessions](system_mode: Boolean) + { + val output_dir: Path = + if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER") + else Path.explode("$ISABELLE_OUTPUT") + + val browser_info: Path = + if (system_mode) Path.explode("~~/browser_info") + else Path.explode("$ISABELLE_BROWSER_INFO") + + private val input_dirs = + if (system_mode) List(output_dir) + else output_dir :: Isabelle_System.find_logics_dirs() + + 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 prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) } + } } diff -r c39614ddb80b -r cd991ba01ffd src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Mar 15 22:01:26 2016 +0100 +++ b/src/Pure/Tools/build.scala Tue Mar 15 23:16:15 2016 +0100 @@ -343,12 +343,8 @@ /* log files */ - private def log(name: String): Path = Path.basic("log") + Path.basic(name) - private def log_gz(name: String): Path = log(name).ext("gz") - private val SESSION_NAME = "\fSession.name = " - sealed case class Log_Info( name: String, stats: List[Properties.T], @@ -465,22 +461,7 @@ def session_sources_stamp(name: String): String = sources_stamp(selected_tree(name).meta_digest :: deps.sources(name)) - - /* persistent information */ - - val (input_dirs, output_dir, browser_info) = - if (system_mode) { - val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER") - (List(output_dir), output_dir, Path.explode("~~/browser_info")) - } - else { - val output_dir = Path.explode("$ISABELLE_OUTPUT") - (output_dir :: Isabelle_System.find_logics_dirs(), output_dir, - Path.explode("$ISABELLE_BROWSER_INFO")) - } - - def find_log(name: String): Option[(Path, Path)] = - input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name))) + val store = Sessions.store(system_mode) /* queue with scheduling information */ @@ -488,11 +469,11 @@ def load_timings(name: String): (List[Properties.T], Double) = { val (path, text) = - find_log(name + ".gz") match { - case Some((_, path)) => (path, File.read_gzip(path)) + store.find_log_gz(name) match { + case Some(path) => (path, File.read_gzip(path)) case None => - find_log(name) match { - case Some((_, path)) => (path, File.read(path)) + store.find_log(name) match { + case Some(path) => (path, File.read(path)) case None => (Path.current, "") } } @@ -520,14 +501,14 @@ /* main build process */ - // prepare log dir - Isabelle_System.mkdirs(output_dir + Path.basic("log")) + store.prepare_output() // optional cleanup if (clean_build) { for (name <- full_tree.graph.all_succs(selected)) { val files = - List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file) + List(Path.basic(name), Sessions.log(name), Sessions.log_gz(name)). + map(store.output_dir + _).filter(_.is_file) if (files.nonEmpty) progress.echo("Cleaning " + name + " ...") if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete") } @@ -573,18 +554,20 @@ val lines = process_result.out_lines.filterNot(_.startsWith("\f")) val tail = job.info.options.int("process_output_tail") val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0) - process_result.copy(out_lines = - "(see also " + (output_dir + log(name)).file.toString + ")" :: lines1) + process_result.copy( + out_lines = + "(see also " + (store.output_dir + Sessions.log(name)).file.toString + ")" :: + lines1) } val heaps = if (process_result.ok) { - (output_dir + log(name)).file.delete + (store.output_dir + Sessions.log(name)).file.delete val heaps = (for (path <- job.output_path; stamp <- time_stamp(path)) yield stamp).toList - File.write_gzip(output_dir + log_gz(name), + File.write_gzip(store.output_dir + Sessions.log_gz(name), Library.terminate_lines( session_sources_stamp(name) :: input_heaps.map(INPUT_HEAP + _) ::: @@ -594,10 +577,11 @@ heaps } else { - (output_dir + Path.basic(name)).file.delete - (output_dir + log_gz(name)).file.delete + (store.output_dir + Path.basic(name)).file.delete + (store.output_dir + Sessions.log_gz(name)).file.delete - File.write(output_dir + log(name), Library.terminate_lines(process_result.out_lines)) + File.write(store.output_dir + Sessions.log(name), + Library.terminate_lines(process_result.out_lines)) progress.echo(name + " FAILED") if (!process_result.interrupted) progress.echo(process_result_tail.out) @@ -613,16 +597,16 @@ val ancestor_results = selected_tree.ancestors(name).map(results(_)) val ancestor_heaps = ancestor_results.map(_.heaps).flatten - val output = output_dir + Path.basic(name) + val output = store.output_dir + Path.basic(name) val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name) val (current, heaps) = { - find_log(name + ".gz") match { - case Some((dir, path)) => - read_stamps(path) match { + store.find(name) match { + case Some((heap, log_gz)) => + read_stamps(log_gz) match { case Some((sources, input_heaps, output_heaps)) => - val heaps = time_stamp(dir + Path.basic(name)).toList + val heaps = time_stamp(heap).toList val current = sources == session_sources_stamp(name) && input_heaps == ancestor_heaps.map(INPUT_HEAP + _) && @@ -647,7 +631,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, browser_info, + new Job(progress, name, info, output, do_output, verbose, store.browser_info, deps(name).session_graph, queue.command_timings(name)) loop(pending, running + (name -> (ancestor_heaps, job)), results) } @@ -687,9 +671,9 @@ map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) for ((chapter, entries) <- browser_chapters) - Present.update_chapter_index(browser_info, chapter, entries) + Present.update_chapter_index(store.browser_info, chapter, entries) - if (browser_chapters.nonEmpty) Present.make_global_index(browser_info) + if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info) } new Build_Results((for ((name, result) <- results.iterator) yield (name, result.process)).toMap)