# HG changeset patch
# User wenzelm
# Date 1477150047 -7200
# Node ID 5f49765a25ec28f9ec399bf6bf300a7434d5e107
# Parent  b89c29ea208f8a64c8b21c69c7973b30026e5da1
process results immediately;

diff -r b89c29ea208f -r 5f49765a25ec src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Oct 22 16:39:27 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 22 17:27:27 2016 +0200
@@ -11,6 +11,8 @@
 import java.time.format.DateTimeFormatter
 import java.util.Locale
 
+import scala.collection.mutable
+
 
 object Build_History
 {
@@ -103,6 +105,7 @@
   def build_history(
     hg: Mercurial.Repository,
     progress: Progress = Ignore_Progress,
+    progress_result: (Process_Result, Path) => Unit = (result: Process_Result, path: Path) => (),
     rev: String = default_rev,
     isabelle_identifier: String = default_isabelle_identifier,
     components_base: String = "",
@@ -254,7 +257,9 @@
 
       first_build = false
 
-      (build_result, log_path.ext("xz"))
+      val res = (build_result, log_path.ext("xz"))
+      progress_result(res._1, res._2)
+      res
     }
   }
 
@@ -343,17 +348,16 @@
 
       val hg = Mercurial.repository(Path.explode(root))
       val progress = new Console_Progress(stderr = true)
+
       val results =
         build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
+          progress_result = (_, log_path) => Output.writeln(log_path.implode, stdout = true),
           components_base = components_base, fresh = fresh, nonfree = nonfree,
           multicore_base = multicore_base, multicore_list = multicore_list, 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_tags = build_tags, build_args = build_args)
 
-      for ((_, log_path) <- results)
-        Output.writeln(log_path.implode, stdout = true)
-
       val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0) sys.exit(rc)
     }
@@ -370,6 +374,7 @@
     isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
     self_update: Boolean = false,
     progress: Progress = Ignore_Progress,
+    progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
     options: String = "",
     args: String = ""): List[(String, Bytes)] =
   {
@@ -393,17 +398,23 @@
 
     /* Admin/build_history */
 
-    val result =
-      ssh.execute(
-        ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
-          ssh.bash_path(isabelle_repos_other) + " " + args,
-        progress_stderr = progress.echo(_)).check
+    val result = new mutable.ListBuffer[(String, Bytes)]
 
-    for (line <- result.out_lines; log = Path.explode(line))
-    yield {
-      val bytes = ssh.read_bytes(log)
+    def progress_stdout(line: String)
+    {
+      val log = Path.explode(line)
+      val res = (log.base.implode, ssh.read_bytes(log))
       ssh.rm(log)
-      (log.base.implode, bytes)
+      progress_result(res._1, res._2)
+      result += res
     }
+
+    ssh.execute(
+      ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
+        ssh.bash_path(isabelle_repos_other) + " " + args,
+      progress_stdout = progress_stdout _,
+      progress_stderr = progress.echo(_)).check
+
+    result.toList
   }
 }
diff -r b89c29ea208f -r 5f49765a25ec src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 22 16:39:27 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 22 17:27:27 2016 +0200
@@ -117,17 +117,18 @@
         using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
           ssh =>
             {
-              val results =
-                Build_History.remote_build_history(ssh,
-                  isabelle_repos,
-                  isabelle_repos.ext(r.host),
-                  isabelle_repos_source = isabelle_dev_source,
-                  self_update = !r.shared_home,
-                  options =
-                    r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
-                  args = "-o timeout=10800 " + r.args)
-              for ((log, bytes) <- results)
-                Bytes.write(logger.log_dir + Path.explode(log), bytes)
+              def progress_result(log_name: String, bytes: Bytes): Unit =
+                Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
+
+              Build_History.remote_build_history(ssh,
+                isabelle_repos,
+                isabelle_repos.ext(r.host),
+                isabelle_repos_source = isabelle_dev_source,
+                self_update = !r.shared_home,
+                progress_result = progress_result _,
+                options =
+                  r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
+                args = "-o timeout=10800 " + r.args)
             })
       })
   }