tuned;
authorwenzelm
Sat, 15 Oct 2016 16:35:50 +0200
changeset 64227 cc2edb86f3cc
parent 64226 65f7d2eea2d7
child 64228 b46969a851a9
tuned;
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Oct 15 16:35:18 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 15 16:35:50 2016 +0200
@@ -330,53 +330,50 @@
 
   /** remote build_history -- via command-line **/
 
-  sealed case class File_Content(name: String, content: Bytes)
-
   def remote_build_history(
-    ssh_session: SSH.Session,
-    isabelle_repos: Path,
-    isabelle_repos_build_history: Path,
-    options: String,
-    args: String,
+    session: SSH.Session,
+    isabelle_repos_self: Path,
+    isabelle_repos_other: Path,
+    isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
+    self_update: Boolean = false,
     progress: Progress = Ignore_Progress,
-    isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
-    self_update: Boolean = false): List[File_Content] =
+    options: String = "",
+    args: String = ""): List[(String, Bytes)] =
   {
-    using(ssh_session.sftp())(sftp =>
+    using(session.sftp())(sftp =>
       {
-        val isabelle_admin = (isabelle_repos + Path.explode("Admin")).implode
+        val isabelle_admin = (isabelle_repos_self + Path.explode("Admin")).implode
 
 
         /* prepare repository clones */
 
-        val ssh = Some(ssh_session)
+        val ssh = Some(session)
 
         val isabelle_hg =
-          if (sftp.stat(isabelle_repos.implode).nonEmpty)
-            Mercurial.repository(isabelle_repos, ssh = ssh)
+          if (sftp.stat(isabelle_repos_self.implode).nonEmpty)
+            Mercurial.repository(isabelle_repos_self, ssh = ssh)
           else
-            Mercurial.clone_repository(isabelle_repos_source, isabelle_repos, ssh = ssh)
+            Mercurial.clone_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
 
         if (self_update) {
           isabelle_hg.pull()
           isabelle_hg.update(clean = true)
-          ssh_session.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
+          session.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
         }
 
-        if (sftp.stat(isabelle_repos_build_history.implode).isEmpty)
-          Mercurial.clone_repository(isabelle_repos.implode, isabelle_repos_build_history, ssh = ssh)
+        if (sftp.stat(isabelle_repos_other.implode).isEmpty)
+          Mercurial.clone_repository(isabelle_repos_self.implode, isabelle_repos_other, ssh = ssh)
 
 
         /* Admin/build_history */
 
         val result =
-          ssh_session.execute(
+          session.execute(
             File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
-              File.bash_path(isabelle_repos_build_history) + " " + args,
+              File.bash_path(isabelle_repos_other) + " " + args,
             progress_stderr = progress.echo(_))
 
-        result.check.out_lines.map(name =>
-          File_Content(Path.explode(name).base.implode, sftp.read_bytes(name)))
+        result.check.out_lines.map(log => (Path.explode(log).base.implode, sftp.read_bytes(log)))
       })
   }
 }