# HG changeset patch
# User wenzelm
# Date 1520078793 -3600
# Node ID 636f633552a3cf85e527b971afe0c754d4dcde2b
# Parent  361d41701de05ed5675468039b0794080ff83c7b
clarified signature: facilitate interactive experimentation;

diff -r 361d41701de0 -r 636f633552a3 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Mar 03 12:54:22 2018 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Mar 03 13:06:33 2018 +0100
@@ -29,11 +29,14 @@
 
 
 
-  /** particular tasks **/
+  /** logger tasks **/
+
+  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
+
 
   /* init and identify Isabelle + AFP repository snapshots */
 
-  private val init =
+  val init =
     Logger_Task("init", logger =>
       {
         Isabelle_Devel.make_index()
@@ -48,7 +51,7 @@
 
   /* build release */
 
-  private val build_release =
+  val build_release =
     Logger_Task("build_release", logger =>
       {
         val rev = Mercurial.repository(isabelle_repos).id()
@@ -61,7 +64,7 @@
 
   /* integrity test of build_history vs. build_history_base */
 
-  private val build_history_base =
+  val build_history_base =
     Logger_Task("build_history_base", logger =>
       {
         val hg =
@@ -294,8 +297,8 @@
           slow = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
 
-  private def remote_build_history(
-    rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task =
+  def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)
+    : Logger_Task =
   {
     val task_name = "build_history-" + r.host
     Logger_Task(task_name, logger =>
@@ -334,9 +337,13 @@
 
   /** task logging **/
 
-  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
+  object Log_Service
+  {
+    def apply(options: Options, progress: Progress = No_Progress): Log_Service =
+      new Log_Service(SSH.init_context(options), progress)
+  }
 
-  class Log_Service private[Isabelle_Cronjob](progress: Progress, val ssh_context: SSH.Context)
+  class Log_Service private(val ssh_context: SSH.Context, progress: Progress)
   {
     current_log.file.delete
 
@@ -433,7 +440,7 @@
 
     /* log service */
 
-    val log_service = new Log_Service(progress, SSH.init_context(Options.init()))
+    val log_service = Log_Service(Options.init(), progress = progress)
 
     def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }