incremental output;
tuned;

--- 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)
         })
     }