# HG changeset patch # User wenzelm # Date 1520075526 -3600 # Node ID 58a33c5684640703e8c9494205d1a59b4ede54b4 # Parent 08dc76bf6400017d5a16abf91750ab865757fccf tuned signature; diff -r 08dc76bf6400 -r 58a33c568464 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) + } + }) }) }