# HG changeset patch
# User wenzelm
# Date 1476353088 -7200
# Node ID 450e06dabdd9e6dfddefe6f362dfb71fe63f798f
# Parent  49816908ae4207c70dcc005923003dd2317665b8
allow to exclude named tasks;

diff -r 49816908ae42 -r 450e06dabdd9 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 11:54:06 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 12:04:48 2016 +0200
@@ -127,7 +127,7 @@
 
   def init_options(): Options = Options.load(Path.explode("~~/Admin/cronjob/cronjob.options"))
 
-  def cronjob(progress: Progress)
+  def cronjob(progress: Progress, exclude_task: Set[String])
   {
     /* soft lock */
 
@@ -151,7 +151,8 @@
 
     def sequential_tasks(tasks: List[Logger_Task])
     {
-      tasks.map(task => log_service.run_task(Date.now(), task))
+      for (task <- tasks.iterator if !exclude_task(task.name))
+        log_service.run_task(Date.now(), task)
     }
 
     def parallel_tasks(tasks: List[Logger_Task])
@@ -164,8 +165,12 @@
           case (_ :: _, remaining) => join(remaining)
         }
       }
+
       val start_date = Date.now()
-      join(tasks.map(task => log_service.fork_task(start_date, task)))
+      val running =
+        for (task <- tasks if !exclude_task(task.name))
+          yield log_service.fork_task(start_date, task)
+      join(running)
     }
 
 
@@ -188,6 +193,7 @@
     Command_Line.tool0 {
       var force = false
       var verbose = false
+      var exclude_task = Set.empty[String]
 
       val getopts = Getopts("""
 Usage: Admin/cronjob/main [OPTIONS]
@@ -195,16 +201,18 @@
   Options are:
     -f           apply force to do anything
     -v           verbose
+    -x NAME      exclude tasks with this name
 """,
         "f" -> (_ => force = true),
-        "v" -> (_ => verbose = true))
+        "v" -> (_ => verbose = true),
+        "x:" -> (arg => exclude_task += arg))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = if (verbose) new Console_Progress() else Ignore_Progress
 
-      if (force) cronjob(progress)
+      if (force) cronjob(progress, exclude_task)
       else error("Need to apply force to do anything")
     }
   }