tuned signature;
authorwenzelm
Sat, 03 Mar 2018 12:12:06 +0100
changeset 67750 58a33c568464
parent 67749 08dc76bf6400
child 67751 361d41701de0
tuned signature;
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 02 20:46:25 2018 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Mar 03 12:12:06 2018 +0100
@@ -130,6 +130,10 @@
     detect: SQL.Source = "",
     active: Boolean = true)
   {
+    def ssh_session(context: SSH.Context): SSH.Session =
+      context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port,
+        proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port)
+
     def sql: SQL.Source =
       Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
       SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
@@ -286,33 +290,30 @@
     val task_name = "build_history-" + r.host
     Logger_Task(task_name, logger =>
       {
-        using(logger.ssh_context.open_session(
-            host = proper_string(r.ssh_host) getOrElse r.host, user = r.user, port = r.port,
-            proxy_host = r.proxy_host, proxy_user = r.proxy_user, proxy_port = r.proxy_port))(
-          ssh =>
-            {
-              val self_update = !r.shared_home
-              val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
+        using(r.ssh_session(logger.ssh_context))(ssh =>
+          {
+            val self_update = !r.shared_home
+            val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
 
-              val results =
-                Build_History.remote_build_history(ssh,
-                  isabelle_repos,
-                  isabelle_repos.ext(r.host),
-                  isabelle_identifier = "cronjob_build_history",
-                  self_update = self_update,
-                  push_isabelle_home = push_isabelle_home,
-                  rev = rev,
-                  afp_rev = afp_rev,
-                  options =
-                    " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
-                    " -f " + r.options,
-                  args = "-o timeout=10800 " + r.args)
+            val results =
+              Build_History.remote_build_history(ssh,
+                isabelle_repos,
+                isabelle_repos.ext(r.host),
+                isabelle_identifier = "cronjob_build_history",
+                self_update = self_update,
+                push_isabelle_home = push_isabelle_home,
+                rev = rev,
+                afp_rev = afp_rev,
+                options =
+                  " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
+                  " -f " + r.options,
+                args = "-o timeout=10800 " + r.args)
 
-              for ((log_name, bytes) <- results) {
-                logger.log(Date.now(), log_name)
-                Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
-              }
-            })
+            for ((log_name, bytes) <- results) {
+              logger.log(Date.now(), log_name)
+              Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
+            }
+          })
       })
   }