diff -r 7f3b6af23513 -r f69ce5e7ea7f src/Pure/Tools/build_history.scala --- a/src/Pure/Tools/build_history.scala Tue Oct 04 15:03:26 2016 +0200 +++ b/src/Pure/Tools/build_history.scala Tue Oct 04 15:42:08 2016 +0200 @@ -21,6 +21,7 @@ private val default_isabelle_identifier = "build_history" def build_history( + progress: Progress, hg: Mercurial.Repository, rev: String = default_rev, isabelle_identifier: String = default_isabelle_identifier, @@ -35,6 +36,12 @@ verbose: Boolean = false, build_args: List[String] = Nil): Process_Result = { + /* output */ + + def output(msg: String) { progress.echo(msg) } + def output_if(b: Boolean, msg: String) { if (b) output(msg) } + + /* sanity checks */ if (threads < 1) error("Bad threads value < 1: " + threads) @@ -53,24 +60,25 @@ /* purge repository */ hg.update(rev = rev, clean = true) - if (verbose) Output.writeln(hg.log(rev, options = "-l1")) + output_if(verbose, hg.log(rev, options = "-l1")) /* invoke isabelle tools */ - def bash(script: String, redirect: Boolean = false): Process_Result = + def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + - " " + script, cwd = hg.root.file, env = null, redirect = redirect) + " " + script, cwd = hg.root.file, env = null, redirect = redirect, + progress_stdout = output_if(echo, _), progress_stderr = output_if(echo, _)) - def isabelle(cmdline: String, redirect: Boolean = false): Process_Result = - bash("bin/isabelle " + cmdline, redirect) + def isabelle(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = + bash("bin/isabelle " + cmdline, redirect, echo) - val isabelle_home_user: Path = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out) + val isabelle_home_user = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out) /* reset settings */ - val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") + val etc_settings = isabelle_home_user + Path.explode("etc/settings") if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) error("Cannot proceed with existing user settings file: " + etc_settings) @@ -160,10 +168,10 @@ /* build */ - isabelle("components -a", redirect = true).check.print_if(verbose) - isabelle("jedit -b" + (if (fresh) " -f" else ""), redirect = true).check.print_if(verbose) + isabelle("components -a", redirect = true, echo = verbose).check + isabelle("jedit -b" + (if (fresh) " -f" else ""), redirect = true, echo = verbose).check - isabelle("build " + File.bash_args(build_args), redirect = true) + isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose) } @@ -236,14 +244,14 @@ error("Repository " + hg + " will be cleaned thoroughly!\n" + "Provide option -A to allow this explicitly.") + val progress = new Console_Progress(false) val res = - build_history(hg, rev = rev, isabelle_identifier = isabelle_identifier, + build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier, components_base = components_base, fresh = fresh, nonfree = nonfree, threads = threads, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, more_settings = more_settings, verbose = verbose, build_args = build_args) - res.print if (!res.ok) sys.exit(res.rc) }) }