# HG changeset patch # User wenzelm # Date 1343143254 -7200 # Node ID 146090de047474ea903ffb585ba9672a1ade0541 # Parent 322fbf5717825a74c43b3278ca61c9037720b707 tuned messages; diff -r 322fbf571782 -r 146090de0474 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Tue Jul 24 17:15:26 2012 +0200 +++ b/src/Pure/System/build.scala Tue Jul 24 17:20:54 2012 +0200 @@ -283,6 +283,10 @@ /** build **/ + private def echo(msg: String) { java.lang.System.out.println(msg) } + private def sleep(): Unit = Thread.sleep(500) + + /* dependencies */ sealed case class Node( @@ -294,7 +298,7 @@ def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources } - def dependencies(queue: Session.Queue): Deps = + def dependencies(verbose: Boolean, queue: Session.Queue): Deps = Deps((Map.empty[String, Node] /: queue.topological_order)( { case (deps, (name, info)) => val preloaded = @@ -304,6 +308,8 @@ } val thy_info = new Thy_Info(new Thy_Load(preloaded)) + if (verbose) echo("Checking " + name) + val thy_deps = thy_info.dependencies( info.theories.map(_._2).flatten. @@ -322,7 +328,7 @@ } thy :: uses }).flatten ::: info.files.map(file => info.dir + file) - val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList + val sources = all_files.map(p => (p, SHA1.digest(p))) deps + (name -> Node(loaded_theories, sources)) })) @@ -399,16 +405,13 @@ /* build */ - private def echo(msg: String) { java.lang.System.out.println(msg) } - private def sleep(): Unit = Thread.sleep(500) - def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int, no_build: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean, more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int = { val options = (Options.init() /: more_options)(_.define_simple(_)) val queue = find_sessions(options, all_sessions, sessions, more_dirs) - val deps = dependencies(queue) + val deps = dependencies(verbose, queue) val (output_dir, browser_info) = if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))