# HG changeset patch
# User wenzelm
# Date 1478469100 -3600
# Node ID ed8940d6295c69da8af9e34edbf7164f94237aa6
# Parent  91c98a58985b9ac0e99c680addac52ce900eadb4
back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;

diff -r 91c98a58985b -r ed8940d6295c src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Nov 06 19:18:24 2016 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Nov 06 22:51:40 2016 +0100
@@ -103,7 +103,6 @@
   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 = "",
@@ -257,9 +256,7 @@
 
       first_build = false
 
-      val res = (build_result, log_path.ext("xz"))
-      progress_result(res._1, res._2)
-      res
+      (build_result, log_path.ext("xz"))
     }
   }
 
@@ -351,7 +348,6 @@
 
       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),
@@ -375,7 +371,6 @@
     self_update: Boolean = false,
     push_isabelle_home: Boolean = false,
     progress: Progress = Ignore_Progress,
-    progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
     options: String = "",
     args: String = ""): (List[(String, Bytes)], Process_Result) =
   {
@@ -418,25 +413,23 @@
 
     /* Admin/build_history */
 
-    var result = Synchronized(List.empty[(String, Bytes)])
-
-    def progress_stdout(line: String)
-    {
-      val log = Path.explode(line)
-      val res = (log.base.implode, ssh.read_bytes(log))
-      ssh.rm(log)
-      progress_result(res._1, res._2)
-      result.change(res :: _)
-    }
-
     val process_result =
       ssh.execute(
         ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
           ssh.bash_path(isabelle_repos_other) + " " + args,
-        progress_stdout = progress_stdout _,
+        progress_stdout = progress.echo(_),
         progress_stderr = progress.echo(_),
         strict = false)
 
-    (result.value.reverse, process_result)
+    val result =
+      for (line <- process_result.out_lines)
+      yield {
+        val log = Path.explode(line)
+        val bytes = ssh.read_bytes(log)
+        ssh.rm(log)
+        (log.base.implode, bytes)
+      }
+
+    (result, process_result)
   }
 }
diff -r 91c98a58985b -r ed8940d6295c src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 06 19:18:24 2016 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 06 22:51:40 2016 +0100
@@ -118,19 +118,19 @@
               val self_update = !r.shared_home
               val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
 
-              def progress_result(log_name: String, bytes: Bytes): Unit =
-                Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
+              val (results, _) =
+                Build_History.remote_build_history(ssh,
+                  isabelle_repos,
+                  isabelle_repos.ext(r.host),
+                  isabelle_repos_source = isabelle_release_source,
+                  self_update = self_update,
+                  push_isabelle_home = push_isabelle_home,
+                  options =
+                    r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
+                  args = "-o timeout=10800 " + r.args)
 
-              Build_History.remote_build_history(ssh,
-                isabelle_repos,
-                isabelle_repos.ext(r.host),
-                isabelle_repos_source = isabelle_release_source,
-                self_update = self_update,
-                push_isabelle_home = push_isabelle_home,
-                progress_result = progress_result _,
-                options =
-                  r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
-                args = "-o timeout=10800 " + r.args)
+              for ((log_name, bytes) <- results)
+                Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
             })
       })
   }