# HG changeset patch # User wenzelm # Date 1354715144 -3600 # Node ID b1dd455593a932731acccd0fa027d49582fb5898 # Parent 82f5aea343e74e608656ddce66ad030b7aa34c95 more formal progress context; diff -r 82f5aea343e7 -r b1dd455593a9 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Wed Dec 05 14:19:44 2012 +0100 +++ b/src/Pure/System/build.scala Wed Dec 05 14:45:44 2012 +0100 @@ -18,6 +18,22 @@ object Build { + /** progress context **/ + + abstract class Progress { + def echo(msg: String): Unit + } + + object Ignore_Progress extends Progress { + override def echo(msg: String) { } + } + + object Console_Progress extends Progress { + override def echo(msg: String) { java.lang.System.out.println(msg) } + } + + + /** session information **/ // external version @@ -263,10 +279,6 @@ /** build **/ - private def echo(msg: String) { java.lang.System.out.println(msg) } - private def sleep(): Unit = Thread.sleep(500) - - /* queue */ object Queue @@ -334,8 +346,8 @@ def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2) } - def dependencies(inlined_files: Boolean, verbose: Boolean, list_files: Boolean, - tree: Session_Tree): Deps = + def dependencies(progress: Build.Progress, inlined_files: Boolean, + verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps = Deps((Map.empty[String, Session_Content] /: tree.topological_order)( { case (deps, (name, info)) => val (preloaded, parent_syntax, parent_errors) = @@ -352,7 +364,7 @@ val groups = if (info.groups.isEmpty) "" else info.groups.mkString(" (", " ", ")") - echo("Session " + name + groups) + progress.echo("Session " + name + groups) } val thy_deps = @@ -371,7 +383,7 @@ }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand) if (list_files) - echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) + progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) val sources = try { all_files.map(p => (p, SHA1.digest(p.file))) } @@ -390,7 +402,7 @@ val options = Options.init val (_, tree) = find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session)) - dependencies(inlined_files, false, false, tree)(session) + dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session) } def outer_syntax(session: String): Outer_Syntax = @@ -537,6 +549,7 @@ /* build */ def build( + progress: Build.Progress, requirements: Boolean = false, all_sessions: Boolean = false, build_heap: Boolean = false, @@ -556,7 +569,7 @@ val (selected, selected_tree) = full_tree.selection(requirements, all_sessions, session_groups, sessions) - val deps = dependencies(true, verbose, list_files, selected_tree) + val deps = dependencies(progress, true, verbose, list_files, selected_tree) val queue = Queue(selected_tree) def make_stamp(name: String): String = @@ -581,14 +594,16 @@ 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) - if (!files.isEmpty) echo("Cleaning " + name + " ...") - if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete") + if (!files.isEmpty) progress.echo("Cleaning " + name + " ...") + if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete") } } // scheduler loop case class Result(current: Boolean, heap: String, rc: Int) + def sleep(): Unit = Thread.sleep(500) + @tailrec def loop( pending: Queue, running: Map[String, (String, Job)], @@ -601,7 +616,7 @@ // finish job val (out, err, rc) = job.join - echo(Library.trim_line(err)) + progress.echo(Library.trim_line(err)) val heap = if (rc == 0) { @@ -619,12 +634,12 @@ (output_dir + log_gz(name)).file.delete File.write(output_dir + log(name), out) - echo(name + " FAILED") + progress.echo(name + " FAILED") if (rc != 130) { - echo("(see also " + (output_dir + log(name)).file.toString + ")") + progress.echo("(see also " + (output_dir + log(name)).file.toString + ")") val lines = split_lines(out) val tail = lines.drop(lines.length - 20 max 0) - echo("\n" + cat_lines(tail)) + progress.echo("\n" + cat_lines(tail)) } no_heap @@ -662,16 +677,16 @@ if (all_current) loop(pending - name, running, results + (name -> Result(true, heap, 0))) else if (no_build) { - if (verbose) echo("Skipping " + name + " ...") + if (verbose) progress.echo("Skipping " + name + " ...") loop(pending - name, running, results + (name -> Result(false, heap, 1))) } else if (parent_result.rc == 0) { - echo((if (do_output) "Building " else "Running ") + name + " ...") + progress.echo((if (do_output) "Building " else "Running ") + name + " ...") val job = new Job(name, info, output, do_output, verbose, browser_info) loop(pending, running + (name -> (parent_result.heap, job)), results) } else { - echo(name + " CANCELLED") + progress.echo(name + " CANCELLED") loop(pending - name, running, results + (name -> Result(false, heap, 1))) } case None => sleep(); loop(pending, running, results) @@ -682,7 +697,7 @@ val results = if (deps.is_empty) { - echo("### Nothing to build") + progress.echo("### Nothing to build") Map.empty } else loop(queue, Map.empty, Map.empty) @@ -692,7 +707,7 @@ val unfinished = (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList .sorted(scala.math.Ordering.String) // FIXME scala-2.10.0-RC1 - echo("Unfinished session(s): " + commas(unfinished)) + progress.echo("Unfinished session(s): " + commas(unfinished)) } rc } @@ -718,8 +733,9 @@ val dirs = select_dirs.map(d => (true, Path.explode(d))) ::: include_dirs.map(d => (false, Path.explode(d))) - build(requirements, all_sessions, build_heap, clean_build, dirs, session_groups, - max_jobs, list_files, no_build, build_options, system_mode, verbose, sessions) + build(Build.Console_Progress, requirements, all_sessions, build_heap, clean_build, + dirs, session_groups, max_jobs, list_files, no_build, build_options, system_mode, + verbose, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } }