# HG changeset patch
# User wenzelm
# Date 1476387882 -7200
# Node ID f38d39c57959d1fbcf6eda5aa3eda0512fefe2c9
# Parent  351b8211aef90e6f5780b2e05213fa13e2700487
clarified;

diff -r 351b8211aef9 -r f38d39c57959 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 21:32:26 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 21:44:42 2016 +0200
@@ -150,51 +150,48 @@
         error("Isabelle cronjob appears to be still running: " + running)
     }
 
-    val main_start_date = Date.now()
+
+    /* log service */
+
     val log_service = new Log_Service(progress)
 
-    File.write(main_state_file, main_start_date + " " + log_service.hostname)
+    def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
+
+    def run_now(task: Logger_Task) { run(Date.now(), task) }
 
 
-    /* run tasks */
-
-    def run(start_date: Date, task: Logger_Task): Unit =
-      log_service.run_task(start_date, task)
+    /* structured tasks */
 
-    def run_sequential(tasks: Logger_Task*): Unit =
+    def SEQ(tasks: Logger_Task*): Logger_Task = Logger_Task(body = _ =>
       for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
-        run(Date.now(), task)
+        run_now(task))
 
-    def run_parallel(tasks: Logger_Task*)
-    {
-      @tailrec def join(running: List[Task])
+    def PAR(tasks: Logger_Task*): Logger_Task = Logger_Task(body = _ =>
       {
-        running.partition(_.is_finished) match {
-          case (Nil, Nil) =>
-          case (Nil, _ :: _) => Thread.sleep(500); join(running)
-          case (_ :: _, remaining) => join(remaining)
+        @tailrec def join(running: List[Task])
+        {
+          running.partition(_.is_finished) match {
+            case (Nil, Nil) =>
+            case (Nil, _ :: _) => Thread.sleep(500); join(running)
+            case (_ :: _, remaining) => join(remaining)
+          }
         }
-      }
-
-      val start_date = Date.now()
-      val running =
-        for (task <- tasks.toList if !exclude_task(task.name))
-          yield log_service.fork_task(start_date, task)
-      join(running)
-    }
-
-    def SEQ(tasks: Logger_Task*): Logger_Task =
-      Logger_Task(body = _ => run_sequential(tasks:_*))
-
-    def PAR(tasks: Logger_Task*): Logger_Task =
-      Logger_Task(body = _ => run_parallel(tasks:_*))
+        val start_date = Date.now()
+        val running =
+          for (task <- tasks.toList if !exclude_task(task.name))
+            yield log_service.fork_task(start_date, task)
+        join(running)
+      })
 
 
     /* main */
 
+    val main_start_date = Date.now()
+    File.write(main_state_file, main_start_date + " " + log_service.hostname)
+
     run(main_start_date,
       Logger_Task("isabelle_cronjob", _ =>
-        run_sequential(isabelle_identify, build_history_base)))
+        run_now(SEQ(isabelle_identify, build_history_base))))
 
     log_service.shutdown()