# HG changeset patch
# User wenzelm
# Date 1476368081 -7200
# Node ID 7a7e370e2523d468c144c1eb4ea02c1e6219f6c7
# Parent  4c0d19b3a882ee44e72ca584b9ebe6d90318b5e1
clarified log_subdir vs. log_filename;
support for sequential and parallel task blocks (unnamed);

diff -r 4c0d19b3a882 -r 7a7e370e2523 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Thu Oct 13 15:44:24 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Oct 13 16:14:41 2016 +0200
@@ -191,8 +191,10 @@
       /* output log */
 
       val log_path =
-        other_isabelle.isabelle_home_user + Path.explode("log") +
-          Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
+        other_isabelle.isabelle_home_user +
+          Build_Log.log_subdir(build_history_date) +
+          Build_Log.log_filename(
+            BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
 
       val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
 
diff -r 4c0d19b3a882 -r 7a7e370e2523 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Oct 13 15:44:24 2016 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu Oct 13 16:14:41 2016 +0200
@@ -27,9 +27,11 @@
       DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
       new java.lang.Long((date.time - date.midnight.time).ms / 1000))
 
-  def log_path(engine: String, date: Date, more: String*): Path =
-    Path.explode(date.rep.getYear.toString) +
-      Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
+  def log_subdir(date: Date): Path =
+    Path.explode("log") + Path.explode(date.rep.getYear.toString)
+
+  def log_filename(engine: String, date: Date, more: String*): Path =
+    Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
 
 
   /* log file collections */
diff -r 4c0d19b3a882 -r 7a7e370e2523 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 15:44:24 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 16:14:41 2016 +0200
@@ -44,7 +44,10 @@
         val isabelle_id = pull_repos(isabelle_repos)
         val afp_id = pull_repos(afp_repos)
 
-        val log_path = log_dir + Build_Log.log_path("isabelle_identify", logger.start_date)
+        val log_path =
+          main_dir +
+            Build_Log.log_subdir(logger.start_date) +
+            Build_Log.log_filename("isabelle_identify", logger.start_date)
         Isabelle_System.mkdirs(log_path.dir)
         File.write(log_path,
           terminate_lines(
@@ -55,10 +58,19 @@
       })
 
 
+  /* build_history_base integrity test */
+
+  val build_history_base =
+    Logger_Task("build_history_base", logger =>
+      {
+        error("FIXME")
+      })
+
+
 
   /** task logging **/
 
-  sealed case class Logger_Task(name: String, body: Logger => Unit)
+  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
 
   class Log_Service private[Isabelle_Cronjob](progress: Progress)
   {
@@ -76,8 +88,9 @@
     val hostname = Isabelle_System.hostname()
 
     def log(date: Date, task_name: String, msg: String): Unit =
-      thread.send(
-        "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
+      if (task_name != "")
+        thread.send(
+          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
 
     def start_logger(start_date: Date, task_name: String): Logger =
       new Logger(this, start_date, task_name)
@@ -148,15 +161,16 @@
     File.write(main_state_file, main_start_date + " " + log_service.hostname)
 
 
-    /* manage tasks */
+    /* run tasks */
+
+    def run(start_date: Date, task: Logger_Task): Unit =
+      log_service.run_task(start_date, task)
 
-    def sequential_tasks(tasks: List[Logger_Task])
-    {
-      for (task <- tasks.iterator if !exclude_task(task.name))
-        log_service.run_task(Date.now(), task)
-    }
+    def run_sequential(tasks: Logger_Task*): Unit =
+      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
+        run(Date.now(), task)
 
-    def parallel_tasks(tasks: List[Logger_Task])
+    def run_parallel(tasks: Logger_Task*)
     {
       @tailrec def join(running: List[Task])
       {
@@ -169,16 +183,23 @@
 
       val start_date = Date.now()
       val running =
-        for (task <- tasks if !exclude_task(task.name))
+        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:_*))
+
 
     /* main */
 
-    log_service.run_task(main_start_date,
-      Logger_Task("isabelle_cronjob", _ => parallel_tasks(List(isabelle_identify))))
+    run(main_start_date,
+      Logger_Task("isabelle_cronjob", _ =>
+        run_sequential(isabelle_identify, build_history_base)))
 
     log_service.shutdown()